{𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : SeminormedRing 𝕜] →
      [inst_1 : AddGroup E] →
        [inst_2 : SMul 𝕜 E] →
          [inst_3 : TopologicalSpace E] →
            {motive : BarrelledSpace 𝕜 E → Sort u} →
              ((continuous_of_lowerSemicontinuous : ∀ (p : Seminorm 𝕜 E), LowerSemicontinuous ⇑p → Continuous ⇑p) →
                  motive ⋯) →
                (t : BarrelledSpace 𝕜 E) → motive t