theorem Th9: :: REAL_3:9

for f being Function holds
( f is sequence of INT iff f is Integer_Sequence )