let f be FinSequence; :: thesis: for n being Nat st n + 1 = len f holds
f = (f | n) ^ <*(f . (n + 1))*>
let n be Nat; :: thesis: ( n + 1 = len f implies f = (f | n) ^ <*(f . (n + 1))*> )
assume A1: n + 1 = len f ; :: thesis: f = (f | n) ^ <*(f . (n + 1))*>
set x = f . (n + 1);
set fn = f | n;
A3: len (f | n) = n by A1, FINSEQ_1:59, NAT_1:11;
A4: dom f = Seg (len f) by FINSEQ_1:def 3;
A5: n <= n + 1 by NAT_1:11;

A6: now :: thesis: for m being Nat st m in dom f holds
f . m = ((f | n) ^ <*(f . (n + 1))*>) . m

let m be Nat; :: thesis: ( m in dom f implies f . m = ((f | n) ^ <*(f . (n + 1))*>) . m )
assume A7: m in dom f ; :: thesis: f . m = ((f | n) ^ <*(f . (n + 1))*>) . m
then A8: 1 <= m by A4, FINSEQ_1:1;
A9: m <= len f by A4, A7, FINSEQ_1:1;

now :: thesis: ( ( m = len f & f . m = ((f | n) ^ <*(f . (n + 1))*>) . m ) or ( m <> len f & ((f | n) ^ <*(f . (n + 1))*>) . m = f . m ) )

per cases ( m = len f or m <> len f ) ;

case m = len f ; :: thesis: f . m = ((f | n) ^ <*(f . (n + 1))*>) . m

hence f . m = ((f | n) ^ <*(f . (n + 1))*>) . m by A1, A3, FINSEQ_1:42; :: thesis: verum

end;

case m <> len f ; :: thesis: ((f | n) ^ <*(f . (n + 1))*>) . m = f . m

then m < n + 1 by A1, A9, XXREAL_0:1;
then A10: m <= n by NAT_1:13;
then 1 <= n by A8, XXREAL_0:2;
then A11: n in dom f by A1, A5, FINSEQ_3:25;
A12: Seg (len (f | n)) = dom (f | n) by FINSEQ_1:def 3;
A13: m in dom (f | n) by A3, A8, A10, FINSEQ_3:25;
hence ((f | n) ^ <*(f . (n + 1))*>) . m = (f | n) . m by FINSEQ_1:def 7
.= f . m by A3, A13, A11, A12, Th6 ;
:: thesis: verum

end;

end;

end;

hence f . m = ((f | n) ^ <*(f . (n + 1))*>) . m ; :: thesis: verum

end;

len ((f | n) ^ <*(f . (n + 1))*>) = n + (len <*(f . (n + 1))*>) by A3, FINSEQ_1:22
.= len f by A1, FINSEQ_1:40 ;
hence f = (f | n) ^ <*(f . (n + 1))*> by A6, FINSEQ_2:9; :: thesis: verum