let Y be set ; 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; ( 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
; g " Y c= rng f
let y be object ; TARSKI:def 3 ( not y in g " Y or y in rng f )
assume A3:
y in g " Y
; 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; verum