for n being Nat
for f being FinSequence of REAL st not (f | n) /^ 1 is empty holds
len ((f | n) /^ 1) < n