{R : Type u_1} →
  {A : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : StarRing R] →
        [inst_2 : MetricSpace R] →
          [inst_3 : IsTopologicalSemiring R] →
            [inst_4 : ContinuousStar R] →
              [inst_5 : NonUnitalRing A] →
                [inst_6 : StarRing A] →
                  [inst_7 : TopologicalSpace A] →
                    [inst_8 : Module R A] →
                      [inst_9 : IsScalarTower R A A] →
                        [inst_10 : SMulCommClass R A A] →
                          {motive : ContinuousMapZero.UniqueHom R A → Sort u} →
                            (t : ContinuousMapZero.UniqueHom R A) →
                              ((eq_of_continuous_of_map_id :
                                    ∀ (s : Set R) [CompactSpace ↑s] [inst_12 : Fact (0 ∈ s)]
                                      (φ ψ : ContinuousMapZero (↑s) R →⋆ₙₐ[R] A),
                                      Continuous ⇑φ →
                                        Continuous ⇑ψ →
                                          φ (ContinuousMapZero.id s) = ψ (ContinuousMapZero.id s) → φ = ψ) →
                                  motive ⋯) →
                                motive t