let i be Nat; :: thesis: for f being FinSequence st f = (*--> 0) . i holds
len f = i
let p be FinSequence; :: thesis: ( p = (*--> 0) . i implies len p = i )
assume A1: p = (*--> 0) . i ; :: thesis: len p = i
p = i |-> 0 by A1, FINSEQ_2:def 6;
hence len p = i by CARD_1:def 7; :: thesis: verum