theorem Th5: :: MSSUBLAT:5

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