let X, Y be non empty set ; :: thesis: for f being Function of X,Y st f is one-to-one holds
for x being Element of X
for A being Subset of X
for B being Subset of Y st f . x in (f .: A) \ B holds
x in A \ (f " B)
let f be Function of X,Y; :: thesis: ( f is one-to-one implies for x being Element of X
for A being Subset of X
for B being Subset of Y st f . x in (f .: A) \ B holds
x in A \ (f " B) )
assume A1: f is one-to-one ; :: thesis: for x being Element of X
for A being Subset of X
for B being Subset of Y st f . x in (f .: A) \ B holds
x in A \ (f " B)
let x be Element of X; :: thesis: for A being Subset of X
for B being Subset of Y st f . x in (f .: A) \ B holds
x in A \ (f " B)
let A be Subset of X; :: thesis: for B being Subset of Y st f . x in (f .: A) \ B holds
x in A \ (f " B)
let B be Subset of Y; :: thesis: ( f . x in (f .: A) \ B implies x in A \ (f " B) )
assume A2: f . x in (f .: A) \ B ; :: thesis: x in A \ (f " B)

A3: now :: thesis: not x in f " B

assume x in f " B ; :: thesis: contradiction
then f . x in B by FUNCT_1:def 7;
hence contradiction by A2, XBOOLE_0:def 5; :: thesis: verum

end;

f . x in f .: A by A2, XBOOLE_0:def 5;
then x in A by A1, Th3;
hence x in A \ (f " B) by A3, XBOOLE_0:def 5; :: thesis: verum