for n being Nat
for f being FinSequence of REAL st n + 1 = len f holds
f /^ n = <*(f . (n + 1))*>