consider a being Element of A;
( {a} c= A & card {a} = 1 ) by CARD_1:50, ZFMISC_1:37;
then A1: ( card B <> 0 & 1 c= card A ) by CARD_1:27;
( card A = card (card A) & card (card B) = card B ) ;
then card (Funcs A,B) = exp (card B),(card A) by FUNCT_5:68;
then exp (card B),1 c= card (Funcs A,B) by A1, CARD_3:139;
then ( card B c= card (Funcs A,B) & not card B is finite ) by CARD_2:40;
then not card (Funcs A,B) is finite ;
hence not Funcs A,B is finite ; :: thesis: verum