let X, Y be set ; :: thesis: ( card X = card Y implies card (2Set X) = card (2Set Y) )
assume card X = card Y ; :: thesis: card (2Set X) = card (2Set Y)
then consider g being Function such that
A1: ( g is one-to-one & dom g = X & rng g = Y ) by CARD_1:5, WELLORD2:def 4;
deffunc H₁( set ) -> Element of $1 = the Element of $1;
deffunc H₂( set ) -> Element of $1 \ {H₁($1)} = the Element of $1 \ {H₁($1)};
deffunc H₃( object ) -> set = {(g . H₁( In ($1,(bool X)))),(g . H₂( In ($1,(bool X))))};
consider f being Function such that
A2: ( dom f = 2Set X & ( for x being object st x in 2Set X holds
f . x = H₃(x) ) ) from FUNCT_1:sch 3();

now :: thesis: for y being object holds
( ( y in rng f implies y in 2Set Y ) & ( y in 2Set Y implies y in rng f ) )

let y be object ; :: thesis: ( ( y in rng f implies y in 2Set Y ) & ( y in 2Set Y implies b₁ in rng f ) )

hereby :: thesis: ( y in 2Set Y implies b₁ in rng f )

assume y in rng f ; :: thesis: y in 2Set Y
then consider x being object such that
A3: ( x in dom f & f . x = y ) by FUNCT_1:def 3;
consider X9 being Subset of X such that
A4: ( x = X9 & card X9 = 2 ) by A2, A3;
A5: y = {(g . H₁( In (X9,(bool X)))),(g . H₂( In (X9,(bool X))))} by A2, A3, A4
.= {(g . H₁(X9)),(g . H₂(X9))} ;
not X9 is trivial

proof

assume A6: X9 is trivial ; :: thesis: contradiction

per cases ( X9 is empty or not X9 is empty ) ;

suppose X9 is empty ; :: thesis: contradiction

hence contradiction by A4; :: thesis: verum

end;

suppose not X9 is empty ; :: thesis: contradiction

then card X9 = 1 by A6, CARD_1:def 7;
hence contradiction by A4; :: thesis: verum

end;

end;

end;

then ( X9 <> {} & X9 \ {H₁(X9)} <> {} ) by ZFMISC_1:139;
then A7: ( H₁(X9) in X9 & H₂(X9) in X9 \ {H₁(X9)} ) ;
then ( H₂(X9) in X9 & not H₂(X9) in {H₁(X9)} ) by XBOOLE_0:def 5;
then ( H₂(X9) in X9 & H₁(X9) <> H₂(X9) ) by TARSKI:def 1;
then A8: g . H₁(X9) <> g . H₂(X9) by A1, A7, FUNCT_1:def 4;
( g . H₁(X9) in Y & g . H₂(X9) in Y ) by A1, A7, FUNCT_1:3;
then A9: {(g . H₁(X9)),(g . H₂(X9))} c= Y by ZFMISC_1:32;
card {(g . H₁(X9)),(g . H₂(X9))} = 2 by A8, CARD_2:57;
hence y in 2Set Y by A5, A9; :: thesis: verum

end;

assume y in 2Set Y ; :: thesis: b₁ in rng f
then consider Y9 being Subset of Y such that
A10: ( y = Y9 & card Y9 = 2 ) ;
consider y1, y2 being object such that
A11: ( y1 <> y2 & Y9 = {y1,y2} ) by A10, CARD_2:60;
( y1 in Y9 & y2 in Y9 ) by A11, TARSKI:def 2;
then A12: ( y1 in rng g & y2 in rng g ) by A1;
then consider x1 being object such that
A13: ( x1 in dom g & g . x1 = y1 ) by FUNCT_1:def 3;
consider x2 being object such that
A14: ( x2 in dom g & g . x2 = y2 ) by A12, FUNCT_1:def 3;
A15: x1 <> x2 by A11, A13, A14;
reconsider X9 = {x1,x2} as Subset of X by A1, A13, A14, ZFMISC_1:32;
card X9 = 2 by A15, CARD_2:57;
then A16: X9 in 2Set X ;

per cases ( H₁(X9) = x1 or H₁(X9) = x2 ) by TARSKI:def 2;

suppose A17: H₁(X9) = x1 ; :: thesis: b₁ in rng f

then X9 \ {H₁(X9)} = {x2} by A15, ZFMISC_1:17;
then A18: H₂(X9) = x2 by TARSKI:def 1;
f . X9 = {(g . H₁( In (X9,(bool X)))),(g . H₂( In (X9,(bool X))))} by A2, A16
.= y by A10, A11, A13, A14, A17, A18 ;
hence y in rng f by A2, A16, FUNCT_1:3; :: thesis: verum

end;

suppose A19: H₁(X9) = x2 ; :: thesis: b₁ in rng f

then X9 \ {H₁(X9)} = {x1} by A15, ZFMISC_1:17;
then A20: H₂(X9) = x1 by TARSKI:def 1;
f . X9 = {(g . H₁( In (X9,(bool X)))),(g . H₂( In (X9,(bool X))))} by A2, A16
.= y by A10, A11, A13, A14, A19, A20 ;
hence y in rng f by A2, A16, FUNCT_1:3; :: thesis: verum

end;

end;

end;

then A21: rng f = 2Set Y by TARSKI:2;

now :: thesis: for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies b₁ = b₂ )
assume A22: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 ) ; :: thesis: b₁ = b₂
then consider X1 being Subset of X such that
A23: ( x1 = X1 & card X1 = 2 ) by A2;
consider X2 being Subset of X such that
A24: ( x2 = X2 & card X2 = 2 ) by A2, A22;
A25: f . x1 = {(g . H₁( In (X1,(bool X)))),(g . H₂( In (X1,(bool X))))} by A2, A22, A23
.= {(g . H₁(X1)),(g . H₂(X1))} ;
A26: f . x2 = {(g . H₁( In (X2,(bool X)))),(g . H₂( In (X2,(bool X))))} by A2, A22, A24
.= {(g . H₁(X2)),(g . H₂(X2))} ;
not X1 is trivial

proof

assume A27: X1 is trivial ; :: thesis: contradiction

per cases ( X1 is empty or not X1 is empty ) ;

suppose X1 is empty ; :: thesis: contradiction

hence contradiction by A23; :: thesis: verum

end;

suppose not X1 is empty ; :: thesis: contradiction

then card X1 = 1 by A27, CARD_1:def 7;
hence contradiction by A23; :: thesis: verum

end;

end;

end;

then ( X1 <> {} & X1 \ {H₁(X1)} <> {} ) by ZFMISC_1:139;
then A28: ( H₁(X1) in X1 & H₂(X1) in X1 \ {H₁(X1)} ) ;
then ( H₂(X1) in X1 & not H₂(X1) in {H₁(X1)} ) by XBOOLE_0:def 5;
then A29: ( H₂(X1) in X1 & H₂(X1) <> H₁(X1) ) by TARSKI:def 1;
A30: ( H₁(X1) in X & H₂(X1) in X ) by A28;
not X2 is trivial

proof

assume A31: X2 is trivial ; :: thesis: contradiction

per cases ( X2 is empty or not X2 is empty ) ;

suppose X2 is empty ; :: thesis: contradiction

hence contradiction by A24; :: thesis: verum

end;

suppose not X2 is empty ; :: thesis: contradiction

then card X2 = 1 by A31, CARD_1:def 7;
hence contradiction by A24; :: thesis: verum

end;

end;

end;

then ( X2 <> {} & X2 \ {H₁(X2)} <> {} ) by ZFMISC_1:139;
then A32: ( H₁(X2) in X2 & H₂(X2) in X2 \ {H₁(X2)} ) ;
then ( H₂(X2) in X2 & not H₂(X2) in {H₁(X2)} ) by XBOOLE_0:def 5;
then A33: ( H₂(X2) in X2 & H₂(X2) <> H₁(X2) ) by TARSKI:def 1;
A34: ( H₁(X2) in X & H₂(X2) in X ) by A32;
A35: ( X1 is finite & X2 is finite ) by A23, A24;
( {H₁(X1),H₂(X1)} c= X1 & card {H₁(X1),H₂(X1)} = 2 ) by A29, ZFMISC_1:32, CARD_2:57;
then A36: {H₁(X1),H₂(X1)} = X1 by A23, A35, CARD_2:102;
( {H₁(X2),H₂(X2)} c= X2 & card {H₁(X2),H₂(X2)} = 2 ) by A33, ZFMISC_1:32, CARD_2:57;
then A37: {H₁(X2),H₂(X2)} = X2 by A24, A35, CARD_2:102;
A38: ( f . x1 in rng f & f . x2 in rng f ) by A22, FUNCT_1:3;
then consider Y1 being Subset of Y such that
A39: ( f . x1 = Y1 & card Y1 = 2 ) by A21;
consider Y2 being Subset of Y such that
A40: ( f . x2 = Y2 & card Y2 = 2 ) by A21, A38;
A41: g . H₁(X1) <> g . H₂(X1)

proof

assume g . H₁(X1) = g . H₂(X1) ; :: thesis: contradiction
then f . x1 = {(g . H₁(X1))} by A25, ENUMSET1:29;
hence contradiction by A39, CARD_1:30; :: thesis: verum

end;

A42: g . H₁(X2) <> g . H₂(X2)

proof

assume g . H₁(X2) = g . H₂(X2) ; :: thesis: contradiction
then f . x2 = {(g . H₁(X2))} by A26, ENUMSET1:29;
hence contradiction by A40, CARD_1:30; :: thesis: verum

end;

A43: {(g . H₁(X1)),(g . H₂(X1))} = {(g . H₁(X2)),(g . H₂(X2))} by A22, A25, A26;

per cases then ( g . H₁(X1) = g . H₁(X2) or g . H₁(X1) = g . H₂(X2) ) by ZFMISC_1:6;

suppose A44: g . H₁(X1) = g . H₁(X2) ; :: thesis: b₁ = b₂

then A45: H₁(X1) = H₁(X2) by A1, A30, A34, FUNCT_1:def 4;
{(g . H₁(X1)),(g . H₂(X1))} \ {(g . H₁(X1))} = {(g . H₂(X1))} by A41, ZFMISC_1:17;
then {(g . H₂(X1))} = {(g . H₂(X2))} by A42, A43, A44, ZFMISC_1:17;
then H₂(X1) = H₂(X2) by A1, A28, A32, FUNCT_1:def 4, ZFMISC_1:3;
hence x1 = x2 by A23, A24, A36, A37, A45; :: thesis: verum

end;

suppose A46: g . H₁(X1) = g . H₂(X2) ; :: thesis: b₁ = b₂

then A47: H₁(X1) = H₂(X2) by A1, A28, A32, FUNCT_1:def 4;
{(g . H₁(X1)),(g . H₂(X1))} \ {(g . H₁(X1))} = {(g . H₂(X1))} by A41, ZFMISC_1:17;
then {(g . H₂(X1))} = {(g . H₁(X2))} by A42, A43, A46, ZFMISC_1:17;
then H₂(X1) = H₁(X2) by A1, A28, A32, FUNCT_1:def 4, ZFMISC_1:3;
hence x1 = x2 by A23, A24, A36, A37, A47; :: thesis: verum

end;

end;

end;

hence card (2Set X) = card (2Set Y) by A2, A21, FUNCT_1:def 4, CARD_1:70; :: thesis: verum