let z be set ; :: thesis: for g, f being Function st z in rng (g * f) holds
z in rng g
let g, f 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 set such that
A1: x in dom (g * f) and
A2: z = (g * f) . x by Def5;
( f . x in dom g & (g * f) . x = g . (f . x) ) by A1, Th21, Th22;
hence z in rng g by A2, Def5; :: thesis: verum