{τ : Type u_1} →
  {inst : TopologicalSpace τ} →
    {inst_1 : AddMonoid τ} →
      {inst_2 : ContinuousAdd τ} →
        {α : Type u_2} →
          {inst_3 : TopologicalSpace α} →
            {P : Sort u} →
              {toFun : τ → α → α} →
                {cont' : Continuous (Function.uncurry toFun)} →
                  {map_add' : ∀ (t₁ t₂ : τ) (x : α), toFun (t₁ + t₂) x = toFun t₁ (toFun t₂ x)} →
                    {map_zero' : ∀ (x : α), toFun 0 x = x} →
                      {toFun' : τ → α → α} →
                        {cont'' : Continuous (Function.uncurry toFun')} →
                          {map_add'' : ∀ (t₁ t₂ : τ) (x : α), toFun' (t₁ + t₂) x = toFun' t₁ (toFun' t₂ x)} →
                            {map_zero'' : ∀ (x : α), toFun' 0 x = x} →
                              { toFun := toFun, cont' := cont', map_add' := map_add', map_zero' := map_zero' } =
                                  { toFun := toFun', cont' := cont'', map_add' := map_add'', map_zero' := map_zero'' } →
                                (toFun ≍ toFun' → P) → P