theorem Th1: :: SEQ_1:1

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