let X1, X2, Y1, Y2 be set ; :: thesis: ( card X1 = card Y1 & card X2 = card Y2 implies card (Funcs (X1,X2)) = card (Funcs (Y1,Y2)) )
assume ( card X1 = card Y1 & card X2 = card Y2 ) ; :: thesis: card (Funcs (X1,X2)) = card (Funcs (Y1,Y2))
then ( X1,Y1 are_equipotent & X2,Y2 are_equipotent ) by CARD_1:5;
hence card (Funcs (X1,X2)) = card (Funcs (Y1,Y2)) by Th53; :: thesis: verum