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 set 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 set ; :: 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:129;
then A3: ( [x,0 ] in H₃(X,Y) & [x,0 ] `1 = x ) by MCART_1:7, XBOOLE_0:def 3;
then x = f . [x,0 ] by A1;
hence x in rng f by A1, A3, FUNCT_1:def 5; :: thesis: verum

end;

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

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

end;

end;

end;

then ( card (X \/ Y) c= card H₃(X,Y) & 0 <> 1 ) by A1, CARD_1:28;
hence card (X \/ Y) c= (card X) +` (card Y) by Th28; :: thesis: verum