∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : NormedSpace ℝ E] {G : Type u_4} [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G] {f g : G → E}
  {f' g' : G →L[ℝ] E} {x : G},
  HasFDerivAt f f' x →
    HasFDerivAt g g' x → HasFDerivAt (fun t => inner 𝕜 (f t) (g t)) ((fderivInnerCLM 𝕜 (f x, g x)).comp (f'.prod g')) x