A1: ( rng f c= ExtREAL & rng g c= ExtREAL ) by VALUED_0:def 2;
rng (f ^ g) = (rng f) \/ (rng g) by FINSEQ_1:44;
then rng (f ^ g) c= ExtREAL by A1, XBOOLE_1:8;
hence f ^ g is extreal-yielding by VALUED_0:def 2; :: thesis: verum