∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] [ContinuousMul α]
  [RegularSpace α] {f : β × γ → α} {g : β → α} {a : α},
  HasProd f a → (∀ (b : β), HasProd (fun c => f (b, c)) (g b)) → HasProd g a