theorem Th6: :: MSSUBLAT:6

for i being Nat
for f being FinSequence st f = (*--> 0) . i holds
len f = i