let f be Real_Sequence; :: thesis: for i being Nat holds (FinSeq (f,i)) ^ <*(f . (i + 1))*> = FinSeq (f,(i + 1))
let i be Nat; :: thesis: (FinSeq (f,i)) ^ <*(f . (i + 1))*> = FinSeq (f,(i + 1))
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

proof

let k be Nat; :: thesis: ( k in dom ((FinSeq (f,i)) ^ <*(f . (i + 1))*>) implies ((FinSeq (f,i)) ^ <*(f . (i + 1))*>) . k = (FinSeq (f,(i + 1))) . k )
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: ((FinSeq (f,i)) ^ <*(f . (i + 1))*>) . k = (FinSeq (f,(i + 1))) . k

per cases then ( k in dom (FinSeq (f,i)) or ex n being Nat st
( n in dom <*(f . (i + 1))*> & k = (len (FinSeq (f,i))) + n ) ) by FINSEQ_1:25;

suppose A3: k in dom (FinSeq (f,i)) ; :: thesis: ((FinSeq (f,i)) ^ <*(f . (i + 1))*>) . k = (FinSeq (f,(i + 1))) . k

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: verum

end;

suppose ex n being Nat st
( n in dom <*(f . (i + 1))*> & k = (len (FinSeq (f,i))) + n ) ; :: thesis: ((FinSeq (f,i)) ^ <*(f . (i + 1))*>) . k = (FinSeq (f,(i + 1))) . k

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: verum

end;

end;

end;

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