for X, X1, X2 being set st X1 misses X2 holds
( Funcs ((X1 \/ X2),X),[:(Funcs (X1,X)),(Funcs (X2,X)):] are_equipotent & card (Funcs ((X1 \/ X2),X)) = card [:(Funcs (X1,X)),(Funcs (X2,X)):] )