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

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