∀ {𝕜 : Type u} {ι : Type v} {ι' : Type v'} {E : ι → Type wE} {E' : ι' → Type wE'} {G : Type wG} [inst : Fintype ι']
  [inst_1 : NontriviallyNormedField 𝕜] [inst_2 : (i : ι) → SeminormedAddCommGroup (E i)]
  [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)] [inst_4 : SeminormedAddCommGroup G] [inst_5 : NormedSpace 𝕜 G]
  [inst_6 : Fintype ι] [inst_7 : (i : ι') → SeminormedAddCommGroup (E' i)] [inst_8 : (i : ι') → NormedSpace 𝕜 (E' i)]
  (f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)) (C : ℝ)
  (H : ∀ (m₁ : (i : ι) → E i) (m₂ : (i : ι') → E' i), ‖(f m₁) m₂‖ ≤ (C * ∏ i, ‖m₁ i‖) * ∏ i, ‖m₂ i‖),
  ‖f.mkContinuousMultilinear C H‖ ≤ max C 0