for f being Function st ( for X1, X2 being set holds f .: (X1 /\ X2) = (f .: X1) /\ (f .: X2) ) holds
f is one-to-one