theorem Th12: :: FRECHET:12

for f, g being Function holds rng (f +* g) = (f .: ((dom f) \ (dom g))) \/ (rng g)