let X, Y be set ; ( ( X,Y are_equipotent or card X = card Y ) implies ( bool X, bool Y are_equipotent & card (bool X) = card (bool Y) ) )
assume
( X,Y are_equipotent or card X = card Y )
; ( bool X, bool Y are_equipotent & card (bool X) = card (bool Y) )
then
X,Y are_equipotent
by CARD_1:5;
then A1:
card (Funcs (X,{0,1})) = card (Funcs (Y,{0,1}))
by FUNCT_5:60;
( card (Funcs (X,{0,1})) = card (bool X) & card (Funcs (Y,{0,1})) = card (bool Y) )
by FUNCT_5:65;
hence
( bool X, bool Y are_equipotent & card (bool X) = card (bool Y) )
by A1, CARD_1:5; verum