[proofplan] We first verify that the product poset is locally finite and that every interval in $P\times Q$ factors as a Cartesian product of intervals in $P$ and $Q$. We then define a candidate Möbius function on comparable pairs of $P\times Q$ by multiplying the two coordinate Möbius functions. The defining cancellation recurrence for the Möbius function separates into a product of two finite coordinate sums, and the recurrence uniquely identifies the candidate with $\mu_{P\times Q}$. [/proofplan]

[step:Show that intervals in the product poset are finite products of coordinate intervals] Let $(a,b),(c,d)\in P\times Q$ satisfy $(a,b)\le (c,d)$ in the product order. For a poset $R$ and comparable elements $u\le v$ in $R$, write \begin{align*} [u,v]_R=\{w\in R:u\le w\le v\} \end{align*} By definition of the product order, this means $a\le c$ in $P$ and $b\le d$ in $Q$. The interval from $(a,b)$ to $(c,d)$ in $P\times Q$ is \begin{align*} [(a,b),(c,d)]_{P\times Q}=\{(r,s)\in P\times Q:a\le r\le c \text{ and } b\le s\le d\}. \end{align*} Hence \begin{align*} [(a,b),(c,d)]_{P\times Q}=[a,c]_P\times [b,d]_Q. \end{align*} Since $P$ and $Q$ are locally finite, the intervals $[a,c]_P$ and $[b,d]_Q$ are finite. Their Cartesian product is finite, so $P\times Q$ is locally finite. [/step]

[step:Define the product candidate for the Möbius function] Let \begin{align*} C_{P\times Q}=\{((p_0,q_0),(p_1,q_1))\in (P\times Q)\times(P\times Q):(p_0,q_0)\le(p_1,q_1)\} \end{align*} denote the comparable-pair domain of $P\times Q$. Define the map \begin{align*} \nu: C_{P\times Q} \to \mathbb{Z}, \qquad ((a,b),(c,d)) \mapsto \mu_P(a,c)\mu_Q(b,d). \end{align*} This is well-defined because $(a,b)\le(c,d)$ implies $a\le c$ and $b\le d$, so both $\mu_P(a,c)$ and $\mu_Q(b,d)$ are defined as integers. We will prove that $\nu$ satisfies the same defining recurrence as the Möbius function of $P\times Q$. [/step]

[step:Factor the cancellation sum into the two coordinate cancellation sums]Fix comparable elements $(a,b)\le(c,d)$ in $P\times Q$. Since the interval factors as $[a,c]_P\times[b,d]_Q$, the finite cancellation sum for $\nu$ is \begin{align*} \sum_{(a,b)\le(r,s)\le(c,d)} \nu((a,b),(r,s)) = \sum_{r\in [a,c]_P}\sum_{s\in [b,d]_Q}\mu_P(a,r)\mu_Q(b,s). \end{align*} Because both sums are finite, we may factor the double sum: \begin{align*} \sum_{r\in [a,c]_P}\sum_{s\in [b,d]_Q}\mu_P(a,r)\mu_Q(b,s) = \left(\sum_{r\in [a,c]_P}\mu_P(a,r)\right) \left(\sum_{s\in [b,d]_Q}\mu_Q(b,s)\right). \end{align*} By the Möbius recursion [citetheorem:8101], applied in the locally finite posets $P$ and $Q$, we have \begin{align*} \sum_{r\in [a,c]_P}\mu_P(a,r)= \begin{cases} 1, & a=c, \end{align*} \begin{align*} 0, & a<c, \end{cases} \end{align*} and \begin{align*} \sum_{s\in [b,d]_Q}\mu_Q(b,s)= \begin{cases} 1, & b=d, \end{align*} \begin{align*} 0, & b<d. \end{cases} \end{align*} Therefore \begin{align*} \sum_{(a,b)\le(r,s)\le(c,d)} \nu((a,b),(r,s))= \begin{cases} 1, & (a,b)=(c,d), \end{align*} \begin{align*} 0, & (a,b)<(c,d). \end{cases} \end{align*}[/step]

[guided]The point of defining $\nu$ as a product is that the interval in the product poset separates into two independent coordinate intervals. Fix $(a,b)\le(c,d)$. From the previous step, \begin{align*} [(a,b),(c,d)]_{P\times Q}=[a,c]_P\times[b,d]_Q. \end{align*} Thus summing over all intermediate elements $(r,s)$ in the product interval is the same as summing over all $r\in [a,c]_P$ and all $s\in [b,d]_Q$: \begin{align*} \sum_{(a,b)\le(r,s)\le(c,d)} \nu((a,b),(r,s)) = \sum_{r\in [a,c]_P}\sum_{s\in [b,d]_Q}\mu_P(a,r)\mu_Q(b,s). \end{align*} This is a finite double sum because $P$ and $Q$ are locally finite. Since the factor $\mu_P(a,r)$ depends only on $r$ and the factor $\mu_Q(b,s)$ depends only on $s$, finite distributivity gives \begin{align*} \sum_{r\in [a,c]_P}\sum_{s\in [b,d]_Q}\mu_P(a,r)\mu_Q(b,s) = \left(\sum_{r\in [a,c]_P}\mu_P(a,r)\right) \left(\sum_{s\in [b,d]_Q}\mu_Q(b,s)\right). \end{align*} Now we use exactly the cancellation recurrence that characterizes the Möbius function. By the Möbius recursion [citetheorem:8101], the first coordinate sum is $1$ when $a=c$ and $0$ when $a<c$: \begin{align*} \sum_{r\in [a,c]_P}\mu_P(a,r)= \begin{cases} 1, & a=c, \end{align*} \begin{align*} 0, & a<c. \end{cases} \end{align*} The same recurrence in $Q$ gives \begin{align*} \sum_{s\in [b,d]_Q}\mu_Q(b,s)= \begin{cases} 1, & b=d, \end{align*} \begin{align*} 0, & b<d. \end{cases} \end{align*} Multiplying these two values handles all cases. If $(a,b)=(c,d)$, then both coordinate sums are $1$, so the product is $1$. If $(a,b)<(c,d)$, then at least one coordinate inequality is strict, so at least one coordinate sum is $0$, and the product is $0$. Hence \begin{align*} \sum_{(a,b)\le(r,s)\le(c,d)} \nu((a,b),(r,s))= \begin{cases} 1, & (a,b)=(c,d), \end{align*} \begin{align*} 0, & (a,b)<(c,d). \end{cases} \end{align*}[/guided]

[step:Use uniqueness in the Möbius recurrence to identify the candidate] The preceding step shows that $\nu$ satisfies the defining left cancellation recurrence for the Möbius function on the locally finite poset $P\times Q$. By the uniqueness part of the Möbius recursion [citetheorem:8101], $\nu=\mu_{P\times Q}$ on every comparable pair in $P\times Q$. Therefore, for every $x\le y$ in $P$ and every $u\le v$ in $Q$, \begin{align*} \mu_{P\times Q}((x,u),(y,v))=\nu((x,u),(y,v))=\mu_P(x,y)\mu_Q(u,v). \end{align*} This is the desired product formula. [/step]