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 ") .: (f .: A) = 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 ") .: (f .: A) = A

let f be Function of X,Y; :: thesis: for A being Subset of X st f is one-to-one holds

(f ") .: (f .: A) = A

let A be Subset of X; :: thesis: ( f is one-to-one implies (f ") .: (f .: A) = A )

A1: dom f = X by FUNCT_2:def 1;

assume f is one-to-one ; :: thesis: (f ") .: (f .: A) = A

hence (f ") .: (f .: A) = A by A1, FUNCT_1:107; :: thesis: verum

for f being Function of X,Y

for A being Subset of X st f is one-to-one holds

(f ") .: (f .: A) = 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 ") .: (f .: A) = A

let f be Function of X,Y; :: thesis: for A being Subset of X st f is one-to-one holds

(f ") .: (f .: A) = A

let A be Subset of X; :: thesis: ( f is one-to-one implies (f ") .: (f .: A) = A )

A1: dom f = X by FUNCT_2:def 1;

assume f is one-to-one ; :: thesis: (f ") .: (f .: A) = A

hence (f ") .: (f .: A) = A by A1, FUNCT_1:107; :: thesis: verum