let X be set ; :: thesis: for Y being non empty set
for f being Function of X,Y st f is one-to-one holds
for B being Subset of X
for C being Subset of Y st C c= f .: B holds
f " C c= B
let Y be non empty set ; :: thesis: for f being Function of X,Y st f is one-to-one holds
for B being Subset of X
for C being Subset of Y st C c= f .: B holds
f " C c= B
let f be Function of X,Y; :: thesis: ( f is one-to-one implies for B being Subset of X
for C being Subset of Y st C c= f .: B holds
f " C c= B )
assume A1: f is one-to-one ; :: thesis: for B being Subset of X
for C being Subset of Y st C c= f .: B holds
f " C c= B
let B be Subset of X; :: thesis: for C being Subset of Y st C c= f .: B holds
f " C c= B
let C be Subset of Y; :: thesis: ( C c= f .: B implies f " C c= B )
assume C c= f .: B ; :: thesis: f " C c= B
then A2: f " C c= f " (f .: B) by RELAT_1:143;
f " (f .: B) c= B by A1, FUNCT_1:82;
hence f " C c= B by A2; :: thesis: verum