ThmDex – An index of mathematical definitions, results, and conjectures.
P3218
By definition \begin{equation} \int_X f \, d \delta_{x_0} = \int_X f^+ \, d \delta_{x_0} - \int_X f^- \, d \delta_{x_0} \end{equation} We may thus use results
(i) R4698: Unsigned basic integral with respect to a point measure
(ii) R1022: Partition of basic function into positive and negative parts

to conclude \begin{equation} \int_X f \, d \delta_{x_0} = \int_X f^+ \, d \delta_{x_0} - \int_X f^- \, d \delta_{x_0} = f^+(x_0) - f^-(x_0) = f(x_0) \end{equation} $\square$