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:68;
consider a being Element of A;
A3: card {a} = 1 by CARD_1:50;
{a} c= A by ZFMISC_1:37;
then 1 c= card A by A3, CARD_1:27;
then exp (card B),1 c= card (Funcs A,B) by A2, CARD_3:139;
hence not Funcs A,B is finite by CARD_2:40; :: thesis: verum