theorem Th1: :: TOPRNS_1:1

for N being Nat
for f being Function holds
( f is Real_Sequence of N iff ( dom f = NAT & ( for n being Nat holds f . n is Point of (TOP-REAL N) ) ) )