let p, q be FinSequence; :: thesis: for A being set holds card ((p ^ q) " A) = (card (p " A)) + (card (q " A))
let A be set ; :: thesis: card ((p ^ q) " A) = (card (p " A)) + (card (q " A))
set X = (p ^ q) " A;
set B = { ((len p) + n) where n is Element of NAT : n in q " A } ;
defpred S₁[ object , object ] means ex i being Nat st
( $1 = i & $2 = (len p) + i );
A1: (p ^ q) " A = (p " A) \/ { ((len p) + n) where n is Element of NAT : n in q " A }

proof

thus (p ^ q) " A c= (p " A) \/ { ((len p) + n) where n is Element of NAT : n in q " A } :: according to XBOOLE_0:def 10 :: thesis: (p " A) \/ { ((len p) + n) where n is Element of NAT : n in q " A } c= (p ^ q) " A

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (p ^ q) " A or x in (p " A) \/ { ((len p) + n) where n is Element of NAT : n in q " A } )
assume A2: x in (p ^ q) " A ; :: thesis: x in (p " A) \/ { ((len p) + n) where n is Element of NAT : n in q " A }
then A3: x in dom (p ^ q) by FUNCT_1:def 7;
then reconsider k = x as Element of NAT ;

now :: thesis: x in (p " A) \/ { ((len p) + n) where n is Element of NAT : n in q " A }

per cases ( k in dom p or ex m being Nat st
( m in dom q & k = (len p) + m ) ) by A3, FINSEQ_1:25;

suppose A4: k in dom p ; :: thesis: x in (p " A) \/ { ((len p) + n) where n is Element of NAT : n in q " A }

then (p ^ q) . k = p . k by FINSEQ_1:def 7;
then p . k in A by A2, FUNCT_1:def 7;
then k in p " A by A4, FUNCT_1:def 7;
hence x in (p " A) \/ { ((len p) + n) where n is Element of NAT : n in q " A } by XBOOLE_0:def 3; :: thesis: verum

end;

suppose ex m being Nat st
( m in dom q & k = (len p) + m ) ; :: thesis: x in (p " A) \/ { ((len p) + n) where n is Element of NAT : n in q " A }

then consider m being Nat such that
A5: m in dom q and
A6: k = (len p) + m ;
q . m = (p ^ q) . k by A5, A6, FINSEQ_1:def 7;
then q . m in A by A2, FUNCT_1:def 7;
then A7: m in q " A by A5, FUNCT_1:def 7;
m in NAT by ORDINAL1:def 12;
then k in { ((len p) + n) where n is Element of NAT : n in q " A } by A6, A7;
hence x in (p " A) \/ { ((len p) + n) where n is Element of NAT : n in q " A } by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence x in (p " A) \/ { ((len p) + n) where n is Element of NAT : n in q " A } ; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (p " A) \/ { ((len p) + n) where n is Element of NAT : n in q " A } or x in (p ^ q) " A )
assume A8: x in (p " A) \/ { ((len p) + n) where n is Element of NAT : n in q " A } ; :: thesis: x in (p ^ q) " A

now :: thesis: x in (p ^ q) " A

per cases ( x in p " A or x in { ((len p) + n) where n is Element of NAT : n in q " A } ) by A8, XBOOLE_0:def 3;

suppose A9: x in p " A ; :: thesis: x in (p ^ q) " A

then A10: x in dom p by FUNCT_1:def 7;
then reconsider k = x as Element of NAT ;
(p ^ q) . k = p . k by A10, FINSEQ_1:def 7;
then A11: (p ^ q) . x in A by A9, FUNCT_1:def 7;
x in dom (p ^ q) by A10, Th22;
hence x in (p ^ q) " A by A11, FUNCT_1:def 7; :: thesis: verum

end;

suppose x in { ((len p) + n) where n is Element of NAT : n in q " A } ; :: thesis: x in (p ^ q) " A

then consider n being Element of NAT such that
A12: x = (len p) + n and
A13: n in q " A ;
A14: n in dom q by A13, FUNCT_1:def 7;
then (p ^ q) . ((len p) + n) = q . n by FINSEQ_1:def 7;
then A15: (p ^ q) . x in A by A12, A13, FUNCT_1:def 7;
x in dom (p ^ q) by A12, A14, FINSEQ_1:28;
hence x in (p ^ q) " A by A15, FUNCT_1:def 7; :: thesis: verum

end;

end;

end;

hence x in (p ^ q) " A ; :: thesis: verum

end;

(p " A) /\ { ((len p) + n) where n is Element of NAT : n in q " A } = {}

proof

set x = the Element of (p " A) /\ { ((len p) + n) where n is Element of NAT : n in q " A } ;
assume A16: not (p " A) /\ { ((len p) + n) where n is Element of NAT : n in q " A } = {} ; :: thesis: contradiction
then the Element of (p " A) /\ { ((len p) + n) where n is Element of NAT : n in q " A } in { ((len p) + n) where n is Element of NAT : n in q " A } by XBOOLE_0:def 4;
then consider n being Element of NAT such that
A17: the Element of (p " A) /\ { ((len p) + n) where n is Element of NAT : n in q " A } = (len p) + n and
A18: n in q " A ;
(len p) + n in p " A by A16, A17, XBOOLE_0:def 4;
then (len p) + n in dom p by FUNCT_1:def 7;
then (len p) + n <= (len p) + 0 by Th25;
then A19: n = 0 by XREAL_1:6;
n in dom q by A18, FUNCT_1:def 7;
hence contradiction by A19, Th24; :: thesis: verum

end;

then A20: p " A misses { ((len p) + n) where n is Element of NAT : n in q " A } ;
reconsider B = { ((len p) + n) where n is Element of NAT : n in q " A } as finite set by A1, FINSET_1:1, XBOOLE_1:7;
A21: card ((p ^ q) " A) = (card (p " A)) + (card B) by A1, A20, CARD_2:40;
A22: for x being object st x in q " A holds
ex y being object st S₁[x,y]

proof

let x be object ; :: thesis: ( x in q " A implies ex y being object st S₁[x,y] )
assume x in q " A ; :: thesis: ex y being object st S₁[x,y]
then x in dom q by FUNCT_1:def 7;
then reconsider i = x as Element of NAT ;
reconsider y = (len p) + i as set ;
take y ; :: thesis: S₁[x,y]
take i ; :: thesis: ( x = i & y = (len p) + i )
thus ( x = i & y = (len p) + i ) ; :: thesis: verum

end;

consider f being Function such that
A23: dom f = q " A and
A24: for x being object st x in q " A holds
S₁[x,f . x] from CLASSES1:sch 1(A22);
A25: rng f = B

proof

thus rng f c= B :: according to XBOOLE_0:def 10 :: thesis: B c= rng f

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in B )
assume x in rng f ; :: thesis: x in B
then consider y being object such that
A26: y in dom f and
A27: f . y = x by FUNCT_1:def 3;
consider i being Nat such that
A28: y = i and
A29: f . y = (len p) + i by A23, A24, A26;
i is Element of NAT by ORDINAL1:def 12;
hence x in B by A23, A26, A27, A28, A29; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in rng f )
assume x in B ; :: thesis: x in rng f
then consider n being Element of NAT such that
A30: x = (len p) + n and
A31: n in q " A ;
ex i being Nat st
( n = i & f . n = (len p) + i ) by A24, A31;
hence x in rng f by A23, A30, A31, FUNCT_1:def 3; :: thesis: verum

end;

f is one-to-one

proof

let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y )
assume that
A32: x in dom f and
A33: y in dom f and
A34: f . x = f . y ; :: thesis: x = y
A35: ex j being Nat st
( y = j & f . y = (len p) + j ) by A23, A24, A33;
ex i being Nat st
( x = i & f . x = (len p) + i ) by A23, A24, A32;
hence x = y by A34, A35; :: thesis: verum

end;

then q " A,B are_equipotent by A23, A25;
hence card ((p ^ q) " A) = (card (p " A)) + (card (q " A)) by A21, CARD_1:5; :: thesis: verum