[proofplan] The hypothesis says that $G$ is obtained from $F$ by summing over the principal order ideal below each point. To recover $F(y)$, we expand the proposed formula $\sum_{x\leq y}G(x)\mu(x,y)$, substitute the defining expression for $G(x)$, and rearrange the resulting finite double sum. The inner coefficient is then exactly the right inverse identity for the Möbius function, so every term cancels except the term indexed by $y$. [/proofplan]

[step:Expand the proposed inverse formula as a finite double sum]Fix an element $y\in P$. For each element $w\in P$, let $w$ denote the lower summation index arising from the expansion of $G(x)$ in the formula below. Since $P$ is finite, all sums are finite and may be rearranged. Using the defining relation for $G$, we compute \begin{align*} \sum_{x\leq y}G(x)\mu(x,y)=\sum_{x\leq y}\left(\sum_{w\leq x}F(w)\right)\mu(x,y). \end{align*} The ordered pairs that occur in this double sum are precisely the pairs $(w,x)\in P\times P$ satisfying $w\leq x\leq y$. Regrouping first by the lower element $w$ gives \begin{align*} \sum_{x\leq y}G(x)\mu(x,y)=\sum_{w\leq y}F(w)\sum_{w\leq x\leq y}\mu(x,y). \end{align*}[/step]

[guided]Fix an element $y\in P$. We want to evaluate the candidate inverse expression \begin{align*} \sum_{x\leq y}G(x)\mu(x,y). \end{align*} For each element $w\in P$, the symbol $w$ will denote the lower summation index that appears when we expand $G(x)$ using the hypothesis. Substituting \begin{align*} G(x)=\sum_{w\leq x}F(w) \end{align*} for each $x\in P$ with $x\leq y$, we obtain \begin{align*} \sum_{x\leq y}G(x)\mu(x,y)=\sum_{x\leq y}\left(\sum_{w\leq x}F(w)\right)\mu(x,y). \end{align*} This is a finite double sum because $P$ is finite. Therefore no convergence theorem is needed: rearrangement is justified by ordinary finite associativity and commutativity of addition in $\mathbb C$. The double sum ranges over exactly the ordered pairs $(w,x)\in P\times P$ such that $w\leq x\leq y$. If we group these pairs by first fixing $w$, then $w$ must satisfy $w\leq y$, and the remaining values of $x$ are exactly those satisfying $w\leq x\leq y$. Hence \begin{align*} \sum_{x\leq y}G(x)\mu(x,y)=\sum_{w\leq y}F(w)\sum_{w\leq x\leq y}\mu(x,y). \end{align*} This form isolates the coefficient of each $F(w)$. The next step is to identify that coefficient using the Möbius inverse identity.[/guided]

[step:Apply the right inverse identity for the Möbius function] For each element $w\in P$ with $w\leq y$, the right inverse identity for the Möbius function, applied to the interval from $w$ to $y$, gives \begin{align*} \sum_{w\leq x\leq y}\mu(x,y)=\mathbb{1}_{\{w=y\}}. \end{align*} Substituting this identity into the regrouped sum yields \begin{align*} \sum_{x\leq y}G(x)\mu(x,y)=\sum_{w\leq y}F(w)\mathbb{1}_{\{w=y\}}. \end{align*} Since $y$ is included in the finite set $\{w\in P:w\leq y\}$ and the indicator is zero for all other elements of that set, the last sum equals $F(y)$. Thus \begin{align*} \sum_{x\leq y}G(x)\mu(x,y)=F(y). \end{align*} Because $y\in P$ was arbitrary, the inversion formula holds for every $y\in P$. [/step]