A1: rng (f ^ g) = (rng f) \/ (rng g) by FINSEQ_1:31;

now :: thesis: for x being object st x in rng (f ^ g) holds
x is complex-valued Function

let x be object ; :: thesis: ( x in rng (f ^ g) implies x is complex-valued Function )
assume x in rng (f ^ g) ; :: thesis: x is complex-valued Function
then ( x in rng f or x in rng g ) by A1, XBOOLE_0:def 3;
hence x is complex-valued Function ; :: thesis: verum

end;

hence f ^ g is complex-functions-valued by VALUED_2:def 2, VALUED_2:def 20; :: thesis: verum