let X, Y be set ; :: thesis: card (X \/ Y) c= (card X) +` (card Y)
consider f being Function such that
A1: ( dom f = H₃(X,Y) & ( for x being object st x in H₃(X,Y) holds
f . x = H₁(x) ) ) from FUNCT_1:sch 3();
X \/ Y c= rng f

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X \/ Y or x in rng f )
assume x in X \/ Y ; :: thesis: x in rng f
then A2: ( x in X or x in Y ) by XBOOLE_0:def 3;

per cases ( x in X or not x in X ) ;

suppose x in X ; :: thesis: x in rng f

then [x,0] in [:X,{0}:] by ZFMISC_1:106;
then A3: [x,0] in H₃(X,Y) by XBOOLE_0:def 3;
[x,0] `1 = x ;
then x = f . [x,0] by A1, A3;
hence x in rng f by A1, A3, FUNCT_1:def 3; :: thesis: verum

end;

suppose not x in X ; :: thesis: x in rng f

then [x,1] in [:Y,{1}:] by A2, ZFMISC_1:106;
then A4: [x,1] in H₃(X,Y) by XBOOLE_0:def 3;
[x,1] `1 = x ;
then x = f . [x,1] by A1, A4;
hence x in rng f by A1, A4, FUNCT_1:def 3; :: thesis: verum

end;

end;

end;

then card (X \/ Y) c= card H₃(X,Y) by A1, CARD_1:12;
hence card (X \/ Y) c= (card X) +` (card Y) by Th16; :: thesis: verum