let n be Nat; :: thesis: for F being set holds
( F is Function of (TOP-REAL n),REAL iff F is Function of (REAL-NS n),REAL )
let F be set ; :: thesis: ( F is Function of (TOP-REAL n),REAL iff F is Function of (REAL-NS n),REAL )
the carrier of (TOP-REAL n) = the carrier of (REAL-NS n) by Th4;
hence ( F is Function of (TOP-REAL n),REAL iff F is Function of (REAL-NS n),REAL ) ; :: thesis: verum