let X, Y be set ; :: thesis: ( ( 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 ) ; :: thesis: ( 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; :: thesis: verum