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 st f . x in f .: A holds
x in A
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 st f . x in f .: A holds
x in A )
assume A1: f is one-to-one ; :: thesis: for x being Element of X
for A being Subset of X st f . x in f .: A holds
x in A
let x be Element of X; :: thesis: for A being Subset of X st f . x in f .: A holds
x in A
let A be Subset of X; :: thesis: ( f . x in f .: A implies x in A )
assume f . x in f .: A ; :: thesis: x in A
then consider y being Element of X such that
A2: y in A and
A3: f . y = f . x by FUNCT_2:116;
thus x in A by A1, A2, A3, FUNCT_2:25; :: thesis: verum