Metamath Proof Explorer


Theorem wrdfn

Description: A word is a function with a zero-based sequence of integers as domain. (Contributed by Alexander van der Vekens, 13-Apr-2018)

Ref Expression
Assertion wrdfn
|- ( W e. Word S -> W Fn ( 0 ..^ ( # ` W ) ) )

Proof

Step Hyp Ref Expression
1 wrdf
 |-  ( W e. Word S -> W : ( 0 ..^ ( # ` W ) ) --> S )
2 1 ffnd
 |-  ( W e. Word S -> W Fn ( 0 ..^ ( # ` W ) ) )