let f, g be Function; :: thesis: rng (f * g) c= rng (f | (rng g))
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (f * g) or y in rng (f | (rng g)) )
assume y in rng (f * g) ; :: thesis: y in rng (f | (rng g))
then consider x being object such that
A1: ( x in dom (f * g) & y = (f * g) . x ) by FUNCT_1:def 3;
A2: ( x in dom g & g . x in dom f ) by A1, FUNCT_1:11;
reconsider z = g . x as set ;
f . z in rng (f | (rng g)) by A2, FUNCT_1:3, FUNCT_1:50;
hence y in rng (f | (rng g)) by A1, FUNCT_1:12; :: thesis: verum