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