theorem Th8: :: REAL_3:8

for f being Function holds
( f is Integer_Sequence iff ( dom f = NAT & ( for x being object st x in NAT holds
f . x is integer ) ) )