{𝕜 : Type u_6} →
  {E : Type u_7} →
    [inst : Zero E] →
      [inst_1 : UniformSpace E] →
        [inst_2 : SeminormedRing 𝕜] →
          [inst_3 : SMul 𝕜 E] →
            {motive : QuasiCompleteSpace 𝕜 E → Sort u} →
              ((quasiComplete : ∀ ⦃s : Set E⦄, Bornology.IsVonNBounded 𝕜 s → IsClosed s → IsComplete s) → motive ⋯) →
                (t : QuasiCompleteSpace 𝕜 E) → motive t