let f be Function; :: thesis:

hereby :: thesis:

assume A1: f is INT -valued ; :: thesis:
let x be object ; :: thesis:

suppose x in dom f ; :: thesis:

then f . x in rng f by FUNCT_1:def 3;
hence f . x is integer by A1; :: thesis:

end;

suppose not x in dom f ; :: thesis:

hence f . x is integer by FUNCT_1:def 2; :: thesis:

end;

end;

end;

assume A2: for x being object holds f . x is integer ; :: thesis:
let y be object ; :: according to TARSKI:def 3,RELAT_1:def 19 :: thesis:
assume y in rng f ; :: thesis:
then consider x being object such that
x in dom f and
A3: f . x = y by FUNCT_1:def 3;
f . x is integer by A2;
hence y in INT by A3, INT_1:def 2; :: thesis: