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:25; :: thesis: verum