let X, Y be set ; :: thesis: ( X misses union Y implies card (UNION (Y,{X})) = card Y )
assume A1: X misses union Y ; :: thesis: card (UNION (Y,{X})) = card Y
deffunc H₁( set ) -> set = $1 \/ X;
consider f being Function such that
A2: ( dom f = Y & ( for A being set st A in Y holds
f . A = H₁(A) ) ) from FUNCT_1:sch 5();
A3: rng f c= UNION (Y,{X})

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in UNION (Y,{X}) )
assume y in rng f ; :: thesis: y in UNION (Y,{X})
then consider x being object such that
A4: ( x in dom f & f . x = y ) by FUNCT_1:def 3;
reconsider x = x as set by TARSKI:1;
X in {X} by TARSKI:def 1;
then H₁(x) in UNION (Y,{X}) by A2, A4, SETFAM_1:def 4;
hence y in UNION (Y,{X}) by A4, A2; :: thesis: verum

end;

UNION (Y,{X}) c= rng f

proof

let xy be object ; :: according to TARSKI:def 3 :: thesis: ( not xy in UNION (Y,{X}) or xy in rng f )
assume xy in UNION (Y,{X}) ; :: thesis: xy in rng f
then consider y, x being set such that
A5: ( y in Y & x in {X} & xy = y \/ x ) by SETFAM_1:def 4;
x = X by A5, TARSKI:def 1;
then f . y = xy by A5, A2;
hence xy in rng f by A2, A5, FUNCT_1:def 3; :: thesis: verum

end;

then A6: UNION (Y,{X}) = rng f by A3;
f is one-to-one

proof

let x be object ; :: according to FUNCT_1:def 4 :: thesis: for b₁ being object holds
( not x in dom f or not b₁ in dom f or not f . x = f . b₁ or x = b₁ )
let y be object ; :: thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y )
assume A7: ( x in dom f & y in dom f & f . x = f . y ) ; :: thesis: x = y
reconsider x = x, y = y as set by TARSKI:1;
A8: ( x misses X & y misses X ) by A1, XBOOLE_1:63, A2, A7, ZFMISC_1:74;
( f . x = H₁(x) & f . y = H₁(y) ) by A7, A2;
hence x = y by A7, A8, XBOOLE_1:71; :: thesis: verum

end;

hence card (UNION (Y,{X})) = card Y by CARD_1:5, A2, A6, WELLORD2:def 4; :: thesis: verum