rng (f +* g) c= (rng f) \/ (rng g) by FUNCT_4:17;
then rng (f +* g) c= NAT by MEMBERED:6;
hence f +* g is natural-valued ; :: thesis: verum