A1: ( rng f c= ExtREAL & rng g c= ExtREAL ) by VALUED_0:def 2;
rng (f ^ g) = (rng f) \/ (rng g) by FINSEQ_1:31;
hence f ^ g is ext-real-valued by A1, XBOOLE_1:8, VALUED_0:def 2; :: thesis: verum