let n be Nat; :: thesis: for f being FinSequence of REAL st n + 1 = len f holds
f /^ n = <*(f . (n + 1))*>
let f be FinSequence of REAL ; :: thesis: ( n + 1 = len f implies f /^ n = <*(f . (n + 1))*> )
assume n + 1 = len f ; :: thesis: f /^ n = <*(f . (n + 1))*>
then (f | n) ^ <*(f . (n + 1))*> = f by RFINSEQ:7
.= (f | n) ^ (f /^ n) by RFINSEQ:8 ;
hence f /^ n = <*(f . (n + 1))*> by FINSEQ_1:33; :: thesis: verum