let n be Nat; :: thesis: ( dom (n NormF) = the carrier of (TOP-REAL n) & dom (n NormF) = REAL n )
thus dom (n NormF) = the carrier of (TOP-REAL n) by FUNCT_2:def 1; :: thesis: dom (n NormF) = REAL n
hence dom (n NormF) = REAL n by EUCLID:22; :: thesis: verum