for m, n being Nat
for f being FinSequence of REAL st n in dom f & 1 <= m & m <= n holds
f . m = (f | n) . m