let X1, Y1, X2, 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:21;
hence card (Funcs X1,X2) = card (Funcs Y1,Y2) by Th67; :: thesis: verum