∀ {α : Type u_1} {β : Type u_2} [inst : CommGroup α] [inst_1 : TopologicalSpace α] {f : β → α}
  (motive : Multipliable f → Prop) (x : Multipliable f), (∀ (w : α) (ha : HasProd f w), motive ⋯) → motive x