let f, g be XFinSequence; :: thesis: for X being set holds card ((f ^ g) " X) = (card (f " X)) + (card (g " X))
let X be set ; :: thesis: card ((f ^ g) " X) = (card (f " X)) + (card (g " X))
(((f ^ g) " X) /\ (len f)) \/ (((f ^ g) " X) \ (len f)) = (f ^ g) " X ;
then A1: card ((f ^ g) " X) = (card (((f ^ g) " X) /\ (len f))) + (card (((f ^ g) " X) \ (len f))) by XBOOLE_1:89, CARD_2:40;
defpred S₁[ object , object ] means ( $1 is Nat & ( for n being Nat st $1 = n holds
$2 = n + (len f) ) );
A2: for x being object st x in g " X holds
ex y being object st
( y in ((f ^ g) " X) \ (len f) & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in g " X implies ex y being object st
( y in ((f ^ g) " X) \ (len f) & S₁[x,y] ) )
assume A3: x in g " X ; :: thesis: ex y being object st
( y in ((f ^ g) " X) \ (len f) & S₁[x,y] )
A4: ( x in dom g & g . x in X ) by A3, FUNCT_1:def 7;
then reconsider x = x as Nat ;
take y = x + (len f); :: thesis: ( y in ((f ^ g) " X) \ (len f) & S₁[x,y] )
( y in dom (f ^ g) & (f ^ g) . y = g . x ) by A4, AFINSQ_1:23, AFINSQ_1:def 3;
then A5: y in (f ^ g) " X by A4, FUNCT_1:def 7;
( not y in Segm (len f) & Segm (len f) = len f ) by NAT_1:11, NAT_1:44, ORDINAL1:def 17;
hence ( y in ((f ^ g) " X) \ (len f) & S₁[x,y] ) by A5, XBOOLE_0:def 5; :: thesis: verum

end;

consider F being Function such that
A6: ( dom F = g " X & rng F c= ((f ^ g) " X) \ (len f) ) and
A7: for x being object st x in g " X holds
S₁[x,F . x] from FUNCT_1:sch 6(A2);
((f ^ g) " X) \ (len f) c= rng F

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ((f ^ g) " X) \ (len f) or x in rng F )
assume A8: x in ((f ^ g) " X) \ (len f) ; :: thesis: x in rng F
A9: ( x in (f ^ g) " X & not x in len f ) by A8, XBOOLE_0:def 5;
A10: ( x in dom (f ^ g) & (f ^ g) . x in X ) by FUNCT_1:def 7, A8;
then reconsider x = x as Nat ;
A11: not x in Segm (len f) by A9, ORDINAL1:def 17;
then A12: x >= len f by NAT_1:44;
A13: x < len (f ^ g) by A10, AFINSQ_1:66;
A14: (f ^ g) . x = g . (x - (len f)) by A12, A10, AFINSQ_1:66, AFINSQ_1:19;
A15: x < (len f) + (len g) by A13, AFINSQ_1:17;
then ( (len f) - (len f) <= x - (len f) & x - (len f) < len g ) by A11, NAT_1:44, XREAL_1:9, XREAL_1:19;
then reconsider xL = x - (len f) as Element of NAT by INT_1:3;
xL in dom g by A15, XREAL_1:19, AFINSQ_1:66;
then A16: xL in g " X by A10, A14, FUNCT_1:def 7;
then ( F . xL = xL + (len f) & xL + (len f) = x ) by A7;
hence x in rng F by A16, A6, FUNCT_1:def 3; :: thesis: verum

end;

then A17: ((f ^ g) " X) \ (len f) = rng F by A6, XBOOLE_0:def 10;
for x1, x2 being object st x1 in dom F & x2 in dom F & F . x1 = F . x2 holds
x1 = x2

proof

let x1, x2 be object ; :: thesis: ( x1 in dom F & x2 in dom F & F . x1 = F . x2 implies x1 = x2 )
assume A18: ( x1 in dom F & x2 in dom F & F . x1 = F . x2 ) ; :: thesis: x1 = x2
( x1 in dom g & x2 in dom g ) by A18, A6, FUNCT_1:def 7;
then reconsider x1 = x1, x2 = x2 as Nat ;
( F . x1 = x1 + (len f) & F . x2 = x2 + (len f) ) by A6, A7, A18;
then x1 + (len f) = x2 + (len f) by A18;
hence x1 = x2 ; :: thesis: verum

end;

then A19: card (g " X) = card (((f ^ g) " X) \ (len f)) by A6, A17, CARD_1:70, FUNCT_1:def 4;
A20: ((f ^ g) " X) /\ (len f) c= f " X

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ((f ^ g) " X) /\ (len f) or x in f " X )
assume A21: x in ((f ^ g) " X) /\ (len f) ; :: thesis: x in f " X
then ( (f ^ g) . x in X & (f ^ g) . x = f . x ) by AFINSQ_1:def 3, FUNCT_1:def 7;
hence x in f " X by A21, FUNCT_1:def 7; :: thesis: verum

end;

f " X c= ((f ^ g) " X) /\ (len f)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in f " X or x in ((f ^ g) " X) /\ (len f) )
assume x in f " X ; :: thesis: x in ((f ^ g) " X) /\ (len f)
then A22: ( x in dom f & dom f c= dom (f ^ g) & f . x in X ) by AFINSQ_1:21, FUNCT_1:def 7;
then ( (f ^ g) . x = f . x & x in dom (f ^ g) ) by AFINSQ_1:def 3;
then x in (f ^ g) " X by A22, FUNCT_1:def 7;
hence x in ((f ^ g) " X) /\ (len f) by XBOOLE_0:def 4, A22; :: thesis: verum

end;

hence card ((f ^ g) " X) = (card (f " X)) + (card (g " X)) by A1, A19, A20, XBOOLE_0:def 10; :: thesis: verum