let D be set ; :: thesis: for f, g being FinSequence of D holds f ^ g = f ^ (FS2XFS g)
let f, g be FinSequence of D; :: thesis: f ^ g = f ^ (FS2XFS g)
A1: len (f ^ g) = (len f) + (len g) by FINSEQ_1:22
.= (len f) + (len (FS2XFS g)) by AFINSQ_1:def 8
.= len (f ^ (FS2XFS g)) by XL1 ;
for k being Nat st k in dom (f ^ g) holds
(f ^ g) . k = (f ^ (FS2XFS g)) . k

proof

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

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

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

then ( (f ^ g) . k = f . k & (f ^ (FS2XFS g)) . k = f . k ) by Def2, FINSEQ_1:def 7;
hence (f ^ g) . k = (f ^ (FS2XFS g)) . k ; :: thesis: verum

end;

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

then consider n being Nat such that
C1: ( n in dom g & k = (len f) + n ) ;
( 1 <= n & n <= len g ) by C1, FINSEQ_3:25;
then reconsider m = n - 1 as Nat ;
C2: m + 1 <= len g by C1, FINSEQ_3:25;
then m < len g by NAT_1:13;
then m in Segm (len g) by NAT_1:44;
then C3: m in Segm (len (FS2XFS g)) by AFINSQ_1:def 8;
(f ^ g) . ((len f) + n) = g . (m + 1) by C1, FINSEQ_1:def 7
.= (FS2XFS g) . m by C2, NAT_1:13, AFINSQ_1:def 8
.= (f ^ (FS2XFS g)) . (((len f) + m) + 1) by C3, Def2 ;
hence (f ^ g) . k = (f ^ (FS2XFS g)) . k by C1; :: thesis: verum

end;

end;

end;

hence f ^ g = f ^ (FS2XFS g) by A1, FINSEQ_3:29; :: thesis: verum