∀ {X : Type u_1} {Y : Type u_2} (R : Type u_4) [inst : Zero X] [inst_1 : Zero Y] [inst_2 : TopologicalSpace X]
  [inst_3 : TopologicalSpace Y] [inst_4 : TopologicalSpace R] [inst_5 : CommSemiring R] [inst_6 : StarRing R]
  [inst_7 : IsTopologicalSemiring R] [inst_8 : ContinuousStar R] (f : ContinuousMapZero X Y)
  (g : ContinuousMapZero Y R), (ContinuousMapZero.nonUnitalStarAlgHom_precomp R f) g = g.comp f