for X1, X2, Y1, Y2 being set st X1,Y1 are_equipotent & X2,Y2 are_equipotent holds
( Funcs (X1,X2), Funcs (Y1,Y2) are_equipotent & card (Funcs (X1,X2)) = card (Funcs (Y1,Y2)) )