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