theorem Th17: :: FUNCT_4:17

for f, g being Function holds rng (f +* g) c= (rng f) \/ (rng g)