let X, Y be non empty set ; :: thesis: for f being Function of X,Y st f is one-to-one holds
for y being Element of Y
for A being Subset of X
for B being Subset of Y st y in (f .: A) \ B holds
(f ") . y in A \ (f " B)
let f be Function of X,Y; :: thesis: ( f is one-to-one implies for y being Element of Y
for A being Subset of X
for B being Subset of Y st y in (f .: A) \ B holds
(f ") . y in A \ (f " B) )
assume A1: f is one-to-one ; :: thesis: for y being Element of Y
for A being Subset of X
for B being Subset of Y st y in (f .: A) \ B holds
(f ") . y in A \ (f " B)
let y be Element of Y; :: thesis: for A being Subset of X
for B being Subset of Y st y in (f .: A) \ B holds
(f ") . y in A \ (f " B)
let A be Subset of X; :: thesis: for B being Subset of Y st y in (f .: A) \ B holds
(f ") . y in A \ (f " B)
let B be Subset of Y; :: thesis: ( y in (f .: A) \ B implies (f ") . y in A \ (f " B) )
assume A2: y in (f .: A) \ B ; :: thesis: (f ") . y in A \ (f " B)
then A3: y in f .: A by XBOOLE_0:def 5;
A4: f .: A c= rng f by RELAT_1:111;
then (f ") . y in dom f by A1, A3, FUNCT_1:32;
then reconsider x = (f ") . y as Element of X ;
y = f . x by A1, A3, A4, FUNCT_1:35;
hence (f ") . y in A \ (f " B) by A1, A2, Th4; :: thesis: verum