∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : Module 𝕜 F] {f : E → F}
  (motive : (IsLinearMap 𝕜 f ∧ ∃ M, 0 < M ∧ ∀ (x : E), ‖f x‖ ≤ M * ‖x‖) → Prop)
  (x : IsLinearMap 𝕜 f ∧ ∃ M, 0 < M ∧ ∀ (x : E), ‖f x‖ ≤ M * ‖x‖),
  (∀ (hl : IsLinearMap 𝕜 f) (hm : ∃ M, 0 < M ∧ ∀ (x : E), ‖f x‖ ≤ M * ‖x‖), motive ⋯) → motive x