∀ {α : Type u_1} {β : Type u_2} [inst : CommGroup α] [inst_1 : UniformSpace α] [IsUniformGroup α] [CompleteSpace α]
  [T2Space α] {f : β → α}, Multipliable f → ∀ (s : Set β), (∏' (x : ↑s), f ↑x) * ∏' (x : ↑sᶜ), f ↑x = ∏' (x : β), f x