thus ( f is integer-valued implies for x being set st x in dom f holds
f . x is integer ) :: thesis: ( ( for x being set st x in dom f holds
f . x is integer ) implies f is integer-valued )

proof

assume A21: f is integer-valued ; :: thesis: for x being set st x in dom f holds
f . x is integer
let x be set ; :: thesis: ( x in dom f implies f . x is integer )
assume A22: x in dom f ; :: thesis: f . x is integer
reconsider f = f as integer-valued Function by A21;
f . x in rng f by A22, FUNCT_1:12;
hence f . x is integer ; :: thesis: verum

end;

assume A23: for x being set st x in dom f holds
f . x is integer ; :: thesis: f is integer-valued
let y be set ; :: according to TARSKI:def 3,VALUED_0:def 5 :: thesis: ( not y in rng f or y in INT )
assume y in rng f ; :: thesis: y in INT
then consider x being set such that
A24: x in dom f and
A25: y = f . x by FUNCT_1:def 5;
y is integer by A23, A24, A25;
hence y in INT by INT_1:def 2; :: thesis: verum