Metamath Proof Explorer

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 ⊢ W ∈ Word V ∧ N ∈ ℤ → W cyclShift N Fn 0 ..^ W

Proof

Step Hyp Ref Expression
1 cshwf ⊢ W ∈ Word V ∧ N ∈ ℤ → W cyclShift N : 0 ..^ W ⟶ V
2 1 ffnd ⊢ W ∈ Word V ∧ N ∈ ℤ → W cyclShift N Fn 0 ..^ W