theorem Th11: :: VALUED_0:11

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