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