Metamath Proof Explorer


Theorem wrdffz

Description: A word is a function from a finite interval of integers. (Contributed by AV, 10-Feb-2021)

Ref Expression
Assertion wrdffz WWordSW:0W1S

Proof

Step Hyp Ref Expression
1 wrdf WWordSW:0..^WS
2 lencl WWordSW0
3 2 nn0zd WWordSW
4 fzoval W0..^W=0W1
5 3 4 syl WWordS0..^W=0W1
6 5 feq2d WWordSW:0..^WSW:0W1S
7 1 6 mpbid WWordSW:0W1S