theorem :: REAL_NS2:17

for n being Nat
for F being set holds
( F is FinSequence of (TOP-REAL n) iff F is FinSequence of (REAL-NS n) ) by Th4;