for n being Nat
for f being FinSequence
for i being non zero Nat holds f . (n + i) = (f /^ n) . i