let i be Nat; :: thesis: for f being FinSequence st f = (*--> 0 ) . i holds
len f = i
A1: i in NAT by ORDINAL1:def 13;
let p be FinSequence; :: thesis: ( p = (*--> 0 ) . i implies len p = i )
assume p = (*--> 0 ) . i ; :: thesis: len p = i
then p = i |-> 0 by A1, PBOOLE:def 20;
hence len p = i by FINSEQ_1:def 18; :: thesis: verum