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 ex y being Element of X st
( y in A & f . y = f . x ) by FUNCT_2:65;
hence x in A by A1, FUNCT_2:19; :: thesis: verum