Theorem repsw

Description: A function mapping a half-open range of nonnegative integers to a constant is a word consisting of one symbol repeated several times ("repeated symbol word"). (Contributed by AV, 4-Nov-2018)

	Ref	Expression
Assertion	repsw	$$⊢\left(S\in V\wedge N\in {\mathbb{N}}_0\right)\to S\mathrm{repeatS}N\in \mathrm{Word}V$$

Proof

Step	Hyp	Ref	Expression
1		repsf	$$⊢\left(S\in V\wedge N\in {\mathbb{N}}_0\right)\to \left(S\mathrm{repeatS}N\right):\left(0..^N\right)⟶V$$
2		iswrdi	$$⊢\left(S\mathrm{repeatS}N\right):\left(0..^N\right)⟶V\to S\mathrm{repeatS}N\in \mathrm{Word}V$$
3	1 2	syl	$$⊢\left(S\in V\wedge N\in {\mathbb{N}}_0\right)\to S\mathrm{repeatS}N\in \mathrm{Word}V$$