let Y be set ; :: thesis: for f, g being Function st Y c= rng (g * f) & g is one-to-one holds
g " Y c= rng f
let f, g be Function; :: thesis: ( Y c= rng (g * f) & g is one-to-one implies g " Y c= rng f )
assume that
A1: Y c= rng (g * f) and
A2: g is one-to-one ; :: thesis: g " Y c= rng f
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in g " Y or y in rng f )
assume A3: y in g " Y ; :: thesis: y in rng f
then A4: y in dom g by FUNCT_1:def 7;
g . y in Y by A3, FUNCT_1:def 7;
then consider x being object such that
A5: x in dom (g * f) and
A6: g . y = (g * f) . x by A1, FUNCT_1:def 3;
A7: x in dom f by A5, FUNCT_1:11;
( g . y = g . (f . x) & f . x in dom g ) by A5, A6, FUNCT_1:11, FUNCT_1:12;
then y = f . x by A2, A4;
hence y in rng f by A7, FUNCT_1:def 3; :: thesis: verum