let X be set ; :: thesis: exp 2,(card X) = card (bool X)
( card (card X) = card X & card 2 = card {{} ,1} ) by CARD_1:88;
hence exp 2,(card X) = card (Funcs X,{{} ,1}) by FUNCT_5:68
.= card (bool X) by FUNCT_5:72 ;
:: thesis: verum