A1: card (card B) = card B ;
card A = card (card A) ;
then A2: card (Funcs (A,B)) = exp ((card B),(card A)) by A1, FUNCT_5:61;
set a = the Element of A;
A3: card { the Element of A} = 1 by CARD_1:30;
{ the Element of A} c= A by ZFMISC_1:31;
then 1 c= card A by A3, CARD_1:11;
then exp ((card B),1) c= card (Funcs (A,B)) by A2, CARD_2:93;
hence not Funcs (A,B) is finite by CARD_2:27; :: thesis: verum