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