{E : Type u_8} →
  [inst : TopologicalSpace E] →
    (enorm : E → ENNReal) →
      Continuous enorm →
        (add : E → E → E) →
          (∀ (a b c : E), a + b + c = a + (b + c)) →
            (zero : E) →
              (∀ (a : E), 0 + a = a) →
                (∀ (a : E), a + 0 = a) →
                  (nsmul : ℕ → E → E) →
                    autoParam (∀ (x : E), nsmul 0 x = 0) AddMonoid.nsmul_zero._autoParam →
                      autoParam (∀ (n : ℕ) (x : E), nsmul (n + 1) x = nsmul n x + x) AddMonoid.nsmul_succ._autoParam →
                        enorm 0 = 0 → (∀ (x y : E), enorm (x + y) ≤ enorm x + enorm y) → ESeminormedAddMonoid E