theorem Th2: :: SEQ_1:2

for f being Function holds
( f is Real_Sequence iff ( dom f = NAT & ( for n being Nat holds f . n is real ) ) )