for i being Nat
for f being FinSequence of {0} holds
( f = i |-> 0 iff len f = i )