let X, Y be set ; :: thesis: for f being one-to-one Function st X misses Y holds
f .: X misses f .: Y
let f be one-to-one Function; :: thesis: ( X misses Y implies f .: X misses f .: Y )
assume Z2: X misses Y ; :: thesis: f .: X misses f .: Y
assume f .: X meets f .: Y ; :: thesis: contradiction
then consider x being object such that
A1: ( x in f .: X & x in f .: Y ) by XBOOLE_0:3;
consider y being object such that
A2: ( y in dom f & y in X & x = f . y ) by A1, FUNCT_1:def 6;
consider z being object such that
A3: ( z in dom f & z in Y & x = f . z ) by A1, FUNCT_1:def 6;
y <> z by Z2, A2, A3, XBOOLE_0:3;
hence contradiction by A3, A2, FUNCT_1:def 4; :: thesis: verum