let f, g be Function; :: thesis: rng g c= rng (f +* g)
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng g or y in rng (f +* g) )
assume y in rng g ; :: thesis: y in rng (f +* g)
then consider x being object such that
A1: ( x in dom g & y = g . x ) by FUNCT_1:def 3;
( x in dom (f +* g) & (f +* g) . x = y ) by A1, Th12, Th13;
hence y in rng (f +* g) by FUNCT_1:def 3; :: thesis: verum