∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : ℕ}
  (c : OrderedFinpartition n) (p : (i : Fin c.length) → ContinuousMultilinearMap 𝕜 (fun i => E) F) (v : Fin n → E)
  (m : Fin c.length), ‖c.applyOrderedFinpartition p v m‖ ≤ ‖p m‖ * ∏ i, ‖v (c.emb m i)‖