let f, g be Function; :: thesis: ( f .: ((dom f) /\ (dom g)) c= rng g implies (rng f) \/ (rng g) = rng (f +* g) )
assume f .: ((dom f) /\ (dom g)) c= rng g ; :: thesis: (rng f) \/ (rng g) = rng (f +* g)
then A1: (rng f) \ (rng g) c= rng (f +* g) by Lm1;
rng g c= rng (f +* g) by FUNCT_4:18;
then ((rng f) \ (rng g)) \/ (rng g) c= rng (f +* g) by A1, XBOOLE_1:8;
then A2: (rng f) \/ (rng g) c= rng (f +* g) by XBOOLE_1:39;
rng (f +* g) c= (rng f) \/ (rng g) by FUNCT_4:17;
hence (rng f) \/ (rng g) = rng (f +* g) by A2, XBOOLE_0:def 10; :: thesis: verum