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