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 ) ) )