now

let u be set ; :: thesis: ( u in rng (f ^ g) implies u in INT )
assume AS: u in rng (f ^ g) ; :: thesis: u in INT
A: rng (f ^ g) = (rng f) \/ (rng g) by FINSEQ_1:44;

now

per cases ( u in rng f or u in rng g ) by AS, A, XBOOLE_0:def 3;

case B: u in rng f ; :: thesis: u in INT

rng f c= INT by VALUED_0:def 5;
hence u in INT by B; :: thesis: verum

end;

case B: u in rng g ; :: thesis: u in INT

rng g c= INT by VALUED_0:def 5;
hence u in INT by B; :: thesis: verum

end;

end;

end;

hence u in INT ; :: thesis: verum

end;

then rng (f ^ g) c= INT by TARSKI:def 3;
hence f ^ g is integer-yielding by VALUED_0:def 5; :: thesis: verum