let f, g be Function; :: thesis: ( rng (g * f) = rng g & g is one-to-one implies dom g c= rng f )
assume that
A1: rng (g * f) = rng g and
A2: g is one-to-one ; :: thesis: dom g c= rng f
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in dom g or y in rng f )
assume A3: y in dom g ; :: thesis: y in rng f
then g . y in rng (g * f) by A1, Def3;
then consider x being object such that
A4: x in dom (g * f) and
A5: g . y = (g * f) . x by Def3;
( (g * f) . x = g . (f . x) & f . x in dom g ) by A4, Th11, Th12;
then A6: y = f . x by A2, A3, A5;
x in dom f by A4, Th11;
hence y in rng f by A6, Def3; :: thesis: verum