rng (f +* g) c= (rng f) \/ (rng g) by FUNCT_4:17;
hence f +* g is ext-natural-valued by XBOOLE_1:1; :: thesis: verum