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 set ; :: 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 13;
g . y in Y by A3, FUNCT_1:def 13;
then consider x being set such that
A5: x in dom (g * f) and
A6: g . y = (g * f) . x by A1, FUNCT_1:def 5;
A7: x in dom f by A5, FUNCT_1:21;
( g . y = g . (f . x) & f . x in dom g ) by A5, A6, FUNCT_1:21, FUNCT_1:22;
then y = f . x by A2, A4, FUNCT_1:def 8;
hence y in rng f by A7, FUNCT_1:def 5; :: thesis: verum