for n being Nat holds
( dom (n NormF) = the carrier of (TOP-REAL n) & dom (n NormF) = REAL n )