A1: ( rng f c= NAT & rng g c= NAT ) by VALUED_0:def 6;
rng (f ^ g) = (rng f) \/ (rng g) by FINSEQ_1:31;
then rng (f ^ g) c= NAT by A1, XBOOLE_1:8;
hence f ^ g is natural-valued by VALUED_0:def 6; :: thesis: verum