let D be set ; :: thesis: for f, g being XFinSequence of D holds XFS2FS (f ^ g) = (XFS2FS f) ^ (XFS2FS g)
let f, g be XFinSequence of D; :: thesis: XFS2FS (f ^ g) = (XFS2FS f) ^ (XFS2FS g)
A1: ( len (XFS2FS (f ^ g)) = len (f ^ g) & len (XFS2FS f) = len f & len (XFS2FS g) = len g ) by AFINSQ_1:def 9;
A1a: ( len (f ^ g) = (len f) + (len g) & len ((XFS2FS f) ^ (XFS2FS g)) = (len (XFS2FS f)) + (len (XFS2FS g)) ) by FINSEQ_1:22, AFINSQ_1:def 3;
then A2: dom (XFS2FS (f ^ g)) = dom ((XFS2FS f) ^ (XFS2FS g)) by A1, FINSEQ_3:29;
for x being Nat st x in dom (XFS2FS (f ^ g)) holds
(XFS2FS (f ^ g)) . x = ((XFS2FS f) ^ (XFS2FS g)) . x

proof

let x be Nat; :: thesis: ( x in dom (XFS2FS (f ^ g)) implies (XFS2FS (f ^ g)) . x = ((XFS2FS f) ^ (XFS2FS g)) . x )
assume B1: x in dom (XFS2FS (f ^ g)) ; :: thesis: (XFS2FS (f ^ g)) . x = ((XFS2FS f) ^ (XFS2FS g)) . x
then B2: ( 1 <= x & x <= len (XFS2FS (f ^ g)) ) by FINSEQ_3:25;
then reconsider k = x - 1 as Nat ;
B3: (XFS2FS (f ^ g)) . x = (f ^ g) . ((k + 1) -' 1) by A1, B2, AFINSQ_1:def 9;

per cases ( x in dom (XFS2FS f) or ex n being Nat st
( n in dom (XFS2FS g) & x = (len (XFS2FS f)) + n ) ) by A2, B1, FINSEQ_1:25;

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

then C2: ( 1 <= x & x <= len (XFS2FS f) ) by FINSEQ_3:25;
k + 1 <= len f by C1, A1, FINSEQ_3:25;
then k < len f by NAT_1:13;
then k in Segm (len f) by NAT_1:44;
then (f ^ g) . k = f . ((k + 1) -' 1) by AFINSQ_1:def 3
.= (XFS2FS f) . (k + 1) by A1, C2, AFINSQ_1:def 9
.= ((XFS2FS f) ^ (XFS2FS g)) . (k + 1) by C1, FINSEQ_1:def 7 ;
hence (XFS2FS (f ^ g)) . x = ((XFS2FS f) ^ (XFS2FS g)) . x by B3; :: thesis: verum

end;

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

then consider n being Nat such that
C1: ( n in dom (XFS2FS g) & x = (len (XFS2FS f)) + n ) ;
C2: ( 1 <= n & n <= len g ) by A1, C1, FINSEQ_3:25;
then reconsider m = n - 1 as Nat ;
m + 1 <= len g by A1, C1, FINSEQ_3:25;
then m < len g by NAT_1:13;
then C2a: m in Segm (len g) by NAT_1:44;
(f ^ g) . ((k + 1) -' 1) = (f ^ g) . (((len f) + n) -' 1) by AFINSQ_1:def 9, C1
.= (f ^ g) . ((((len f) + m) + 1) -' 1)
.= g . ((m + 1) -' 1) by C2a, AFINSQ_1:def 3
.= (XFS2FS g) . (m + 1) by C2, AFINSQ_1:def 9
.= ((XFS2FS f) ^ (XFS2FS g)) . x by C1, FINSEQ_1:def 7 ;
hence (XFS2FS (f ^ g)) . x = ((XFS2FS f) ^ (XFS2FS g)) . x by A1, B2, AFINSQ_1:def 9; :: thesis: verum

end;

end;

end;

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