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

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