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