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