[proofplan]
We use the defining cancellation identities for the Möbius function on finite intervals. The forward implication substitutes the zeta-sum formula for $g(x)$ into the Möbius transform, reindexes the resulting finite double sum over pairs $u\le x\le y$, and uses right cancellation to leave only the coefficient of $f(y)$. The converse performs the symmetric substitution into $\sum_{x\le y}f(x)$ and uses left cancellation to leave only $g(y)$.
[/proofplan]
[step:Record the two cancellation identities on each interval]
Fix $u,y\in P$ with $u\le y$. Since $P$ is locally finite, the interval
\begin{align*}
[u,y]=\{x\in P:u\le x\le y\}
\end{align*}
is finite. By the Möbius recursion and cancellation identities [citetheorem:8101], applied in this finite interval, we have the integer identity
\begin{align*}
\sum_{u\le x\le y}\mu_P(u,x)=1
\end{align*}
when $u=y$, and the integer identity
\begin{align*}
\sum_{u\le x\le y}\mu_P(u,x)=0
\end{align*}
when $u<y$. Interpreting each integer as the corresponding endomorphism of the abelian group $A$, this means that, for every $a\in A$,
\begin{align*}
\left(\sum_{u\le x\le y}\mu_P(u,x)\right)a=a
\end{align*}
if $u=y$, and equals the zero element $0_A\in A$ if $u<y$.
The same cited cancellation identities also give the right-handed form
\begin{align*}
\sum_{u\le x\le y}\mu_P(x,y)=1
\end{align*}
when $u=y$, and
\begin{align*}
\sum_{u\le x\le y}\mu_P(x,y)=0
\end{align*}
when $u<y$.
[/step]
[step:Substitute the zeta sum for $g$ and use right cancellation]
Assume first that
\begin{align*}
g(y)=\sum_{x\le y}f(x)
\end{align*}
for every $y\in P$. Fix $y\in P$. By the finiteness hypothesis, the following sums are finite, so finite distributivity and reindexing in the abelian group $A$ are valid. We compute
\begin{align*}
\sum_{x\le y}\mu_P(x,y)g(x)=\sum_{x\le y}\mu_P(x,y)\sum_{u\le x}f(u)
\end{align*}
and reindex over all pairs $(u,x)$ satisfying $u\le x\le y$:
\begin{align*}
\sum_{x\le y}\mu_P(x,y)g(x)=\sum_{u\le y}\left(\sum_{u\le x\le y}\mu_P(x,y)\right)f(u).
\end{align*}
For a fixed $u\le y$, the inner coefficient is $1$ if $u=y$ and $0$ if $u<y$, by the right cancellation identity from the previous step. Hence every term vanishes except the term with $u=y$, and therefore
\begin{align*}
\sum_{x\le y}\mu_P(x,y)g(x)=f(y).
\end{align*}
Since $y\in P$ was arbitrary, the [Möbius inversion formula](/theorems/1749) holds for every $y\in P$.
[guided]
Assume that $g$ is obtained from $f$ by summing over lower sets:
\begin{align*}
g(y)=\sum_{x\le y}f(x)
\end{align*}
for every $y\in P$. We want to prove that applying the Möbius coefficients recovers $f$. Fix an element $y\in P$. The hypothesis that all sums appearing in the theorem are finite is used here: it lets us expand and regroup finite sums in the abelian group $A$ without invoking any convergence notion.
Start with the proposed inverse transform at $y$:
\begin{align*}
\sum_{x\le y}\mu_P(x,y)g(x).
\end{align*}
For each fixed $x\le y$, substitute the assumed formula for $g(x)$:
\begin{align*}
\sum_{x\le y}\mu_P(x,y)g(x)=\sum_{x\le y}\mu_P(x,y)\sum_{u\le x}f(u).
\end{align*}
This is a finite sum over pairs $(u,x)$ with $u\le x\le y$. We regroup it by first choosing $u$ and then summing over all intermediate elements $x$ between $u$ and $y$:
\begin{align*}
\sum_{x\le y}\mu_P(x,y)g(x)=\sum_{u\le y}\left(\sum_{u\le x\le y}\mu_P(x,y)\right)f(u).
\end{align*}
The reason this regrouping is useful is that the inner coefficient is exactly a Möbius cancellation sum. If $u=y$, the only element $x$ with $u\le x\le y$ is $x=y$, so the coefficient is $\mu_P(y,y)=1$. If $u<y$, the right cancellation identity from [citetheorem:8101] gives
\begin{align*}
\sum_{u\le x\le y}\mu_P(x,y)=0.
\end{align*}
Thus the coefficient of $f(u)$ is zero for every $u<y$, while the coefficient of $f(y)$ is one. Therefore
\begin{align*}
\sum_{x\le y}\mu_P(x,y)g(x)=f(y).
\end{align*}
Because $y$ was arbitrary, the inverse formula holds for all $y\in P$.
[/guided]
[/step]
[step:Substitute the Möbius sum for $f$ and use left cancellation]
Conversely, assume that
\begin{align*}
f(y)=\sum_{x\le y}\mu_P(x,y)g(x)
\end{align*}
for every $y\in P$. Fix $y\in P$. Using the finiteness hypothesis, substitute this formula into the lower-set sum of $f$ and reindex the resulting finite double sum:
\begin{align*}
\sum_{x\le y}f(x)=\sum_{x\le y}\sum_{u\le x}\mu_P(u,x)g(u).
\end{align*}
Hence
\begin{align*}
\sum_{x\le y}f(x)=\sum_{u\le y}\left(\sum_{u\le x\le y}\mu_P(u,x)\right)g(u).
\end{align*}
For each fixed $u\le y$, the inner coefficient is $1$ if $u=y$ and $0$ if $u<y$, by the left cancellation identity from the first step. Therefore only the term $u=y$ remains, and we obtain
\begin{align*}
\sum_{x\le y}f(x)=g(y).
\end{align*}
Since $y\in P$ was arbitrary, the original summation formula for $g$ holds for every $y\in P$. This proves the equivalence.
[/step]
