Theorem cshwrn

Description: The range of a cyclically shifted word is a subset of the set of symbols for the word. (Contributed by AV, 12-Nov-2018)

	Ref	Expression
Assertion	cshwrn	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) → ran ( 𝑊 cyclShift 𝑁 ) ⊆ 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		cshwf	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) → ( 𝑊 cyclShift 𝑁 ) : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝑉 )
2	1	frnd	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) → ran ( 𝑊 cyclShift 𝑁 ) ⊆ 𝑉 )