theorem :: FINSEQ_5:30

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