Theorem cshwfn

Description: A cyclically shifted word is a function with a half-open range of integers of the same length as the word as domain. (Contributed by AV, 12-Nov-2018)

	Ref	Expression
Assertion	cshwfn	$$⊢\left(W\in \mathrm{Word}V\wedge N\in \mathbb{Z}\right)\to \left(W\mathrm{cyclShift}N\right)Fn\left(0..^\left|W\right|\right)$$

Proof

Step	Hyp	Ref	Expression
1		cshwf	$$⊢\left(W\in \mathrm{Word}V\wedge N\in \mathbb{Z}\right)\to \left(W\mathrm{cyclShift}N\right):\left(0..^\left|W\right|\right)⟶V$$
2	1	ffnd	$$⊢\left(W\in \mathrm{Word}V\wedge N\in \mathbb{Z}\right)\to \left(W\mathrm{cyclShift}N\right)Fn\left(0..^\left|W\right|\right)$$