∀ {X : Type u_2} [inst : TopologicalSpace X] {A : Type u_1} [inst_1 : Ring A] [inst_2 : StarRing A]
  [inst_3 : Algebra ℝ A] (φ : C(X, NNReal) →⋆ₐ[NNReal] A) (f g : C(X, ℝ)),
  φ (f + g).toNNReal - φ (-(f + g)).toNNReal = φ f.toNNReal - φ (-f).toNNReal + (φ g.toNNReal - φ (-g).toNNReal)