theorem Th15: :: REAL_NS1:15

for n being Nat
for f being set holds
( f is sequence of (REAL-NS n) iff f is sequence of (REAL-US n) )