let f be Real_Sequence; :: thesis:
let i be Nat; :: thesis:
set f1 = FinSeq (f,i);
set g = <*(f . (i + 1))*>;
set h = FinSeq (f,(i + 1));
dom (FinSeq (f,i)) = Seg i by Th19;
then Seg (len (FinSeq (f,i))) = Seg i by FINSEQ_1:def 3;
then A0: len (FinSeq (f,i)) = i by FINSEQ_1:6;
A1: dom ((FinSeq (f,i)) ^ <*(f . (i + 1))*>) = Seg ((len (FinSeq (f,i))) + (len <*(f . (i + 1))*>)) by FINSEQ_1:def 7
.= Seg (i + 1) by FINSEQ_1:39, A0
.= dom (FinSeq (f,(i + 1))) by Th19 ;
for k being Nat st k in dom ((FinSeq (f,i)) ^ <*(f . (i + 1))*>) holds
((FinSeq (f,i)) ^ <*(f . (i + 1))*>) . k = (FinSeq (f,(i + 1))) . k

let k be Nat; :: thesis:
i <= i + 1 by NAT_1:13;
then A2: Seg i c= Seg (i + 1) by FINSEQ_1:5;
assume k in dom ((FinSeq (f,i)) ^ <*(f . (i + 1))*>) ; :: thesis:

then A4: k in Seg i by Th19;
((FinSeq (f,i)) ^ <*(f . (i + 1))*>) . k = (FinSeq (f,i)) . k by FINSEQ_1:def 7, A3
.= f . k by A4, FUNCT_1:49
.= (FinSeq (f,(i + 1))) . k by A2, A4, FUNCT_1:49 ;
hence ((FinSeq (f,i)) ^ <*(f . (i + 1))*>) . k = (FinSeq (f,(i + 1))) . k ; :: thesis:

end;

then consider n being Nat such that
A5: ( n in dom <*(f . (i + 1))*> & k = (len (FinSeq (f,i))) + n ) ;
n in Seg 1 by A5, FINSEQ_1:def 8;
then A6: n = 1 by TARSKI:def 1, FINSEQ_1:2;
1 <= i + 1 by NAT_1:12;
hence ((FinSeq (f,i)) ^ <*(f . (i + 1))*>) . k = (FinSeq (f,(i + 1))) . k by FUNCT_1:49, FINSEQ_1:1, A0, A5, A6; :: thesis:

end;

hence (FinSeq (f,i)) ^ <*(f . (i + 1))*> = FinSeq (f,(i + 1)) by A1, FINSEQ_1:13; :: thesis: