∀ {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {E : Type u_2} {F : Type u_3} {G : Type u_4}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F]
  [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G] [inst_6 : CompleteSpace G] (B : F →L[ℝ] E →L[ℝ] G)
  [inst_7 : CompleteSpace E],
  m ≤ mΩ →
    ∀ [MeasureTheory.IsFiniteMeasure μ] {f : Ω → F} {g : Ω → E},
      MeasureTheory.StronglyMeasurable f →
        MeasureTheory.Integrable g μ →
          ∀ (c : ℝ), (∀ᵐ (ω : Ω) ∂μ, ‖f ω‖ ≤ c) → μ[fun ω => (B (f ω)) (g ω) | m] =ᵐ[μ] fun ω => (B (f ω)) (μ[g | m] ω)