let n be Nat; :: thesis: for f being n + 1 -element FinSequence holds f = (f | n) ^ <*(f . (n + 1))*>
let f be n + 1 -element FinSequence; :: thesis: f = (f | n) ^ <*(f . (n + 1))*>
A0: ( len f = n + 1 & n + 1 > n + 0 ) by CARD_1:def 7, XREAL_1:6;
then A0a: len f = (len (f | n)) + 1 by FINSEQ_1:59
.= len ((f | n) ^ <*(f . (n + 1))*>) by FINSEQ_2:16 ;
for k being Nat st k in dom f holds
f . k = ((f | n) ^ <*(f . (n + 1))*>) . k

proof

let k be Nat; :: thesis: ( k in dom f implies f . k = ((f | n) ^ <*(f . (n + 1))*>) . k )
assume k in dom f ; :: thesis: f . k = ((f | n) ^ <*(f . (n + 1))*>) . k
then B2: ( 1 <= k & k <= len f ) by FINSEQ_3:25;

per cases then ( k < n + 1 or k = n + 1 ) by A0, XXREAL_0:1;

suppose k < n + 1 ; :: thesis: f . k = ((f | n) ^ <*(f . (n + 1))*>) . k

then C1: k <= n by NAT_1:13;
len (f | n) = n by CARD_1:def 7;
then k in dom (f | n) by B2, C1, FINSEQ_3:25;
then ((f | n) ^ <*(f . (n + 1))*>) . k = (f | n) . k by FINSEQ_1:def 7
.= f . k by C1, B2, FINSEQ_1:1, FUNCT_1:49 ;
hence f . k = ((f | n) ^ <*(f . (n + 1))*>) . k ; :: thesis: verum

end;

suppose C1: k = n + 1 ; :: thesis: f . k = ((f | n) ^ <*(f . (n + 1))*>) . k

len (f | n) = n by CARD_1:def 7;
hence f . k = ((f | n) ^ <*(f . (n + 1))*>) . k by C1; :: thesis: verum

end;

end;

end;

hence f = (f | n) ^ <*(f . (n + 1))*> by A0a, FINSEQ_3:29; :: thesis: verum