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

proof

let x be Nat; :: thesis: ( x in dom (FS2XFS (f ^ g)) implies (FS2XFS (f ^ g)) . x = ((FS2XFS f) ^ (FS2XFS g)) . x )
assume B1: x in dom (FS2XFS (f ^ g)) ; :: thesis: (FS2XFS (f ^ g)) . x = ((FS2XFS f) ^ (FS2XFS g)) . x
then B1a: x in Segm (len (FS2XFS (f ^ g))) ;
then B2: (FS2XFS (f ^ g)) . x = (f ^ g) . (x + 1) by A1, NAT_1:44, AFINSQ_1:def 8;

per cases ( x in dom (FS2XFS f) or ex k being Nat st
( k in dom (FS2XFS g) & x = (len (FS2XFS f)) + k ) ) by A1, A1a, B1, AFINSQ_1:20;

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

then C1a: x in Segm (len (FS2XFS f)) ;
then ( 0 <= x & x < len (FS2XFS f) ) by NAT_1:44;
then ( 0 + 1 <= x + 1 & x + 1 <= len f ) by A1, NAT_1:13;
then x + 1 in dom f by FINSEQ_3:25;
then (f ^ g) . (x + 1) = f . (x + 1) by FINSEQ_1:def 7
.= (FS2XFS f) . x by A1, C1a, NAT_1:44, AFINSQ_1:def 8
.= ((FS2XFS f) ^ (FS2XFS g)) . x by C1, AFINSQ_1:def 3 ;
hence (FS2XFS (f ^ g)) . x = ((FS2XFS f) ^ (FS2XFS g)) . x by B1a, A1, NAT_1:44, AFINSQ_1:def 8; :: thesis: verum

end;

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

then consider k being Nat such that
C1: ( k in dom (FS2XFS g) & x = (len (FS2XFS f)) + k ) ;
C1a: k in Segm (len (FS2XFS g)) by C1;
then k < len g by A1, NAT_1:44;
then ( 0 + 1 <= k + 1 & k + 1 <= len g ) by NAT_1:13;
then k + 1 in dom g by FINSEQ_3:25;
then (f ^ g) . ((len f) + (k + 1)) = g . (k + 1) by FINSEQ_1:def 7
.= (FS2XFS g) . k by C1a, A1, NAT_1:44, AFINSQ_1:def 8
.= ((FS2XFS f) ^ (FS2XFS g)) . (k + (len f)) by A1, C1, AFINSQ_1:def 3 ;
hence (FS2XFS (f ^ g)) . x = ((FS2XFS f) ^ (FS2XFS g)) . x by A1, B2, C1; :: thesis: verum

end;

end;

end;

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