theorem Th18: :: REAL_NS2:18

for n being Nat
for F being set holds
( F is Function of (TOP-REAL n),REAL iff F is Function of (REAL-NS n),REAL )