now :: thesis: for u being object st u in rng (f ^ g) holds

u in INT

then
rng (f ^ g) c= INT
by TARSKI:def 3;u in INT

let u be object ; :: thesis: ( u in rng (f ^ g) implies u in INT )

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

assume A2: u in rng (f ^ g) ; :: thesis: u in INT

hence u in INT ; :: thesis: verum

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

assume A2: u in rng (f ^ g) ; :: thesis: u in INT

hence u in INT ; :: thesis: verum

hence f ^ g is INT -valued by RELAT_1:def 19; :: thesis: verum