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