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