let X be set ; :: thesis: ( bool X, bool (card X) are_equipotent & card (bool X) = card (bool (card X)) )
consider f being Function such that
A1: f is one-to-one and
A2: dom f = X and
A3: rng f = card X by CARD_1:def 2, WELLORD2:def 4;
deffunc H1( set ) -> set = f .: $1;
consider g being Function such that
A4: ( dom g = bool X & ( for x being set st x in bool X holds
g . x = H1(x) ) ) from FUNCT_1:sch 5();
 thus bool X, bool (card X) are_equipotent :: thesis: card (bool X) = card (bool (card X))
proof
take g ; :: according to WELLORD2:def 4 :: thesis: ( g is one-to-one & proj1 g = bool X & proj2 g = bool (card X) )
thus g is one-to-one :: thesis: ( proj1 g = bool X & proj2 g = bool (card X) )
proof
let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in proj1 g or not y in proj1 g or not g . x = g . y or x = y )
assume that
A5: x in dom g and
A6: y in dom g and
A7: g . x = g . y ; :: thesis: x = y
reconsider xx = x, yy = y as set by TARSKI:1;
A8: ( g . x = f .: xx & g . y = f .: yy ) by A4, A5, A6;
A9: yy c= xx
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in yy or z in xx )
assume A10: z in yy ; :: thesis: z in xx
then f . z in f .: yy by A2, A4, A6, FUNCT_1:def 6;
then ex u being object st
( u in dom f & u in xx & f . z = f . u ) by A7, A8, FUNCT_1:def 6;
hence z in xx by A1, A2, A4, A6, A10; :: thesis: verum
end;
xx c= yy
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in xx or z in yy )
assume A11: z in xx ; :: thesis: z in yy
then f . z in f .: xx by A2, A4, A5, FUNCT_1:def 6;
then ex u being object st
( u in dom f & u in yy & f . z = f . u ) by A7, A8, FUNCT_1:def 6;
hence z in yy by A1, A2, A4, A5, A11; :: thesis: verum
end;
hence x = y by A9, XBOOLE_0:def 10; :: thesis: verum
end;
thus dom g = bool X by A4; :: thesis: proj2 g = bool (card X)
thus rng g c= bool (card X) :: according to XBOOLE_0:def 10 :: thesis: bool (card X) c= proj2 g
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng g or x in bool (card X) )
assume x in rng g ; :: thesis: x in bool (card X)
then consider y being object such that
A12: y in dom g and
A13: x = g . y by FUNCT_1:def 3;
reconsider y = y as set by TARSKI:1;
A14: f .: y c= rng f by RELAT_1:111;
g . y = f .: y by A4, A12;
hence x in bool (card X) by A3, A13, A14; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in bool (card X) or x in proj2 g )
reconsider xx = x as set by TARSKI:1;
A15: f " xx c= dom f by RELAT_1:132;
assume x in bool (card X) ; :: thesis: x in proj2 g
then f .: (f " xx) = x by A3, FUNCT_1:77;
then g . (f " xx) = x by A2, A4, A15;
hence x in proj2 g by A2, A4, A15, FUNCT_1:def 3; :: thesis: verum
end;
hence card (bool X) = card (bool (card X)) by CARD_1:5; :: thesis: verum