let D be set ; :: thesis: for f, g being XFinSequence of D holds f ^ g = f ^ (XFS2FS g)
let f, g be XFinSequence of D; :: thesis: f ^ g = f ^ (XFS2FS g)
A1: len (f ^ g) = (len f) + (len g) by AFINSQ_1:17
.= (len f) + (len (XFS2FS g)) by AFINSQ_1:def 9
.= len (f ^ (XFS2FS g)) by XL1 ;
for k being Nat st k in dom (f ^ g) holds
(f ^ g) . k = (f ^ (XFS2FS g)) . k

proof

let k be Nat; :: thesis: ( k in dom (f ^ g) implies (f ^ g) . k = (f ^ (XFS2FS g)) . k )
assume k in dom (f ^ g) ; :: thesis: (f ^ g) . k = (f ^ (XFS2FS g)) . k

per cases then ( k in dom f or ex n being Nat st
( n in dom g & k = (len f) + n ) ) by AFINSQ_1:20;

suppose k in dom f ; :: thesis: (f ^ g) . k = (f ^ (XFS2FS g)) . k

then ( (f ^ g) . k = f . k & (f ^ (XFS2FS g)) . k = f . k ) by Def1, AFINSQ_1:def 3;
hence (f ^ g) . k = (f ^ (XFS2FS g)) . k ; :: thesis: verum

end;

suppose ex n being Nat st
( n in dom g & k = (len f) + n ) ; :: thesis: (f ^ g) . k = (f ^ (XFS2FS g)) . k

then consider n being Nat such that
C1: ( n in dom g & k = (len f) + n ) ;
n in Segm (len g) by C1;
then n < len g by NAT_1:44;
then C2: ( 0 + 1 <= n + 1 & n + 1 <= len g ) by NAT_1:13;
then n + 1 in Seg (len g) ;
then n + 1 in Seg (len (XFS2FS g)) by AFINSQ_1:def 9;
then C3: n + 1 in dom (XFS2FS g) by FINSEQ_1:def 3;
(f ^ g) . ((len f) + n) = g . ((n + 1) - 1) by C1, AFINSQ_1:def 3
.= (XFS2FS g) . (n + 1) by C2, AFINSQ_1:def 9
.= (f ^ (XFS2FS g)) . (((len f) + (n + 1)) - 1) by C3, Def1 ;
hence (f ^ g) . k = (f ^ (XFS2FS g)) . k by C1; :: thesis: verum

end;

end;

end;

hence f ^ g = f ^ (XFS2FS g) by A1; :: thesis: verum