theorem Th11: :: VALUED_0:11

for f being Function holds
( f is INT -valued iff for x being object holds f . x is integer )