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

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