∀ {𝕜 : Type u_5} {D : Type u_1} {E : Type u_2} {F : Type u_4} {G : Type u_3} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F]
  [inst_4 : NontriviallyNormedField 𝕜] [inst_5 : NormedAlgebra ℝ 𝕜] [inst_6 : NormedAddCommGroup D]
  [inst_7 : NormedSpace ℝ D] [inst_8 : NormedAddCommGroup G] [inst_9 : NormedSpace ℝ G] [inst_10 : NormedSpace 𝕜 F]
  [inst_11 : NormedSpace 𝕜 E] [inst_12 : NormedSpace 𝕜 G] (B : E →L[𝕜] F →L[𝕜] G) {g : D → F},
  Function.HasTemperateGrowth g →
    ∀ (n : ℕ × ℕ),
      ∃ s C,
        0 ≤ C ∧
          ∀ (f : SchwartzMap D E) (x : D),
            ‖x‖ ^ n.1 * ‖iteratedFDeriv ℝ n.2 (fun x => (B (f x)) (g x)) x‖ ≤
              C * (s.sup (schwartzSeminormFamily 𝕜 D E)) f