let f, g be Function; :: thesis: rng (f * g) c= rng (f | (rng g))
let y be set ; :: 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 set such that
C1: ( x in dom (f * g) & y = (f * g) . x ) by FUNCT_1:def 5;
C2: ( x in dom g & g . x in dom f ) by FUNCT_1:21, C1;
reconsider z = g . x as set ;
f . z in rng (f | (rng g)) by FUNCT_1:73, C2, FUNCT_1:12;
hence y in rng (f | (rng g)) by FUNCT_1:22, C1; :: thesis: verum