∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : NonUnitalSemiring β] [inst_2 : StarRing β]
  [inst_3 : TopologicalSpace β] [inst_4 : ContinuousStar β] [inst_5 : IsTopologicalSemiring β]
  (f g : CompactlySupportedContinuousMap α β), star (f * g) = star g * star f