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:21;
then A1: card (Funcs X,{0 ,1}) = card (Funcs Y,{0 ,1}) by FUNCT_5:67;
( card (Funcs X,{0 ,1}) = card (bool X) & card (Funcs Y,{0 ,1}) = card (bool Y) ) by FUNCT_5:72;
hence ( bool X, bool Y are_equipotent & card (bool X) = card (bool Y) ) by A1, CARD_1:21; :: thesis: verum