rng (f +* g) c= (rng f) \/ (rng g) by FUNCT_4:18;
then rng (f +* g) is ext-real-membered ;
then rng (f +* g) c= ExtREAL by MEMBERED:2;
hence f +* g is ext-real-valued by Def2; :: thesis: verum