let X, Y be set ; card (X \/ Y) c= (card X) +` (card Y)
consider f being Function such that
A1:
( dom f = H3(X,Y) & ( for x being object st x in H3(X,Y) holds
f . x = H1(x) ) )
from FUNCT_1:sch 3();
X \/ Y c= rng f
proof
let x be
object ;
TARSKI:def 3 ( not x in X \/ Y or x in rng f )
assume
x in X \/ Y
;
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
not
x in X
;
x in rng fthen
[x,1] in [:Y,{1}:]
by A2, ZFMISC_1:106;
then A4:
[x,1] in H3(
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;
verum end; end;
end;
then
card (X \/ Y) c= card H3(X,Y)
by A1, CARD_1:12;
hence
card (X \/ Y) c= (card X) +` (card Y)
by Th16; verum