now :: thesis: for u being object st u in rng (f ^ g) holds
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

now :: thesis: ( ( u in rng f & u in INT ) or ( u in rng g & u in INT ) )

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

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

rng f c= INT by RELAT_1:def 19;
hence u in INT by A3; :: thesis: verum

end;

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

rng g c= INT by RELAT_1:def 19;
hence u in INT by A4; :: 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 INT -valued by RELAT_1:def 19; :: thesis: verum