let X be set ; :: thesis: for Y being non empty set
for f being Function of X,Y
for A being Subset of X st f is one-to-one holds
f .: (A `) c= (f .: A) `
let Y be non empty set ; :: thesis: for f being Function of X,Y
for A being Subset of X st f is one-to-one holds
f .: (A `) c= (f .: A) `
let f be Function of X,Y; :: thesis: for A being Subset of X st f is one-to-one holds
f .: (A `) c= (f .: A) `
let A be Subset of X; :: thesis: ( f is one-to-one implies f .: (A `) c= (f .: A) ` )
assume A1: f is one-to-one ; :: thesis: f .: (A `) c= (f .: A) `
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in f .: (A `) or e in (f .: A) ` )
assume A2: e in f .: (A `) ; :: thesis: e in (f .: A) `
then reconsider y = e as Element of Y ;
consider x1 being object such that
A3: x1 in X and
A4: x1 in A ` and
A5: y = f . x1 by A2, FUNCT_2:64;
assume not e in (f .: A) ` ; :: thesis: contradiction
then A6: ex x2 being object st
( x2 in X & x2 in A & y = f . x2 ) by FUNCT_2:64, SUBSET_1:29;
not x1 in A by A4, XBOOLE_0:def 5;
hence contradiction by A1, A3, A5, A6, FUNCT_2:19; :: thesis: verum