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