let X, Y be set ; :: thesis: for f being Function st X misses Y & f is one-to-one holds
f .: X misses f .: Y
let f be Function; :: thesis: ( X misses Y & f is one-to-one implies f .: X misses f .: Y )
assume ( X /\ Y = {} & f is one-to-one ) ; :: according to XBOOLE_0:def 7 :: thesis: f .: X misses f .: Y
then ( f .: (X /\ Y) = {} & f .: (X /\ Y) = (f .: X) /\ (f .: Y) ) by Th61;
hence f .: X misses f .: Y ; :: thesis: verum