[proofplan] The value on the diagonal is one of the defining properties of the Möbius function. For a strict interval $x<y$, we use the defining left-cancellation identity for the Möbius function on the finite interval $[x,y]$. Local finiteness makes the interval finite, so we may separate the last term $z=y$ from the sum and solve for $\mu_P(x,y)$. [/proofplan] [step:Read the diagonal value from the definition of the Möbius function] Assume first that $x=y$. By the definition of the Möbius function of a locally finite poset, its diagonal values satisfy \begin{align*} \mu_P(x,x)=1. \end{align*} Since $x=y$, this gives \begin{align*} \mu_P(x,y)=1. \end{align*} [/step] [step:Isolate the endpoint term in the defining cancellation identity] Assume now that $x<y$. Since $P$ is locally finite, the interval \begin{align*} [x,y]:=\{z\in P:x\le z\le y\} \end{align*} is finite. Hence every sum over elements of $[x,y]$ is finite. By the defining left-cancellation identity for the Möbius function, applied to the comparable pair $x<y$, we have \begin{align*} \sum_{x\le z\le y}\mu_P(x,z)=0. \end{align*} Because the summation set is finite and decomposes as the disjoint union of $\{z\in P:x\le z<y\}$ and $\{y\}$, this identity becomes \begin{align*} \sum_{x\le z<y}\mu_P(x,z)+\mu_P(x,y)=0. \end{align*} Subtracting the finite sum from both sides gives \begin{align*} \mu_P(x,y)=-\sum_{x\le z<y}\mu_P(x,z). \end{align*} [guided] Assume $x<y$. The point of local finiteness is that the interval between $x$ and $y$ contains only finitely many elements. More explicitly, define \begin{align*} [x,y]:=\{z\in P:x\le z\le y\}. \end{align*} Since $P$ is locally finite, this set is finite, so the sum over $x\le z\le y$ is an ordinary finite sum. The Möbius function $\mu_P$ is defined as the inverse of the zeta function in the incidence algebra of $P$. In the left-cancellation form of that definition, for every strict pair $x<y$ one has \begin{align*} \sum_{x\le z\le y}\mu_P(x,z)=0. \end{align*} We apply this identity to the fixed strict pair $x<y$ under consideration. Now separate the summation term with endpoint $z=y$ from the remaining terms. The finite indexing set $\{z\in P:x\le z\le y\}$ is the disjoint union of the set $\{z\in P:x\le z<y\}$ and the singleton $\{y\}$. Therefore \begin{align*} \sum_{x\le z\le y}\mu_P(x,z)=\sum_{x\le z<y}\mu_P(x,z)+\mu_P(x,y). \end{align*} Combining this decomposition with the cancellation identity gives \begin{align*} \sum_{x\le z<y}\mu_P(x,z)+\mu_P(x,y)=0. \end{align*} Solving this equality for the endpoint term $\mu_P(x,y)$ yields \begin{align*} \mu_P(x,y)=-\sum_{x\le z<y}\mu_P(x,z). \end{align*} This is exactly the recursive formula. [/guided] [/step] [step:Combine the two cases] The case $x=y$ gives the diagonal value $\mu_P(x,y)=1$, and the case $x<y$ gives the recursive formula \begin{align*} \mu_P(x,y)=-\sum_{x\le z<y}\mu_P(x,z). \end{align*} These two cases exhaust all comparable pairs $x\le y$ in $P$, so the theorem follows. [/step]