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) and
A2: y = (f +* g) . x by FUNCT_1:def 3;
( ( x in dom f & not x in dom g ) or x in dom g ) by A1, Th12;
then ( ( x in dom f & (f +* g) . x = f . x ) or ( x in dom g & (f +* g) . x = g . x ) ) by Th11, Th13;
then ( y in rng f or y in rng g ) by A2, FUNCT_1:def 3;
hence y in (rng f) \/ (rng g) by XBOOLE_0:def 3; :: thesis: verum