∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Zero β] [inst_2 : TopologicalSpace β]
  (toContinuousMap : C(α, β)) (zero_at_infty' : Filter.Tendsto toContinuousMap.toFun (Filter.cocompact α) (nhds 0))
  (toContinuousMap_1 : C(α, β))
  (zero_at_infty'_1 : Filter.Tendsto toContinuousMap_1.toFun (Filter.cocompact α) (nhds 0)),
  ({ toContinuousMap := toContinuousMap, zero_at_infty' := zero_at_infty' } =
      { toContinuousMap := toContinuousMap_1, zero_at_infty' := zero_at_infty'_1 }) =
    (toContinuousMap = toContinuousMap_1)