let z be object ; :: thesis: for f, g being Function st z in rng (g * f) holds
z in rng g
let f, g be Function; :: thesis: ( z in rng (g * f) implies z in rng g )
assume z in rng (g * f) ; :: thesis: z in rng g
then consider x being object such that
A1: x in dom (g * f) and
A2: z = (g * f) . x by Def3;
( f . x in dom g & (g * f) . x = g . (f . x) ) by A1, Th11, Th12;
hence z in rng g by A2, Def3; :: thesis: verum