{E : Type u_8} →
  [inst : TopologicalSpace E] →
    (enorm : E → ENNReal) →
      Continuous enorm →
        (mul : E → E → E) →
          (∀ (a b c : E), a * b * c = a * (b * c)) →
            (one : E) →
              (∀ (a : E), 1 * a = a) →
                (∀ (a : E), a * 1 = a) →
                  (npow : ℕ → E → E) →
                    autoParam (∀ (x : E), npow 0 x = 1) Monoid.npow_zero._autoParam →
                      autoParam (∀ (n : ℕ) (x : E), npow (n + 1) x = npow n x * x) Monoid.npow_succ._autoParam →
                        enorm 1 = 0 → (∀ (x y : E), enorm (x * y) ≤ enorm x + enorm y) → ESeminormedMonoid E