theorem :: NEWTON04:4

for n being Nat
for D being set
for f being b₂ -valued FinSequence st n >= len f holds
len (f | n) = len f