[proofplan]
The proof is a direct unpacking of the definitions. We evaluate noncommutative $*$-polynomials at the tuple $(a_1,\dots,a_n)$ using the canonical evaluation $*$-homomorphism. The normalization condition for a state gives the value of the joint $*$-law on the unit, and the positivity condition for a state gives non-negativity on every polynomial square $P^*P$.
[/proofplan]
[step:Introduce the evaluation $*$-homomorphism at the tuple]
Let
\begin{align*}
\operatorname{ev}_a: \mathbb C\langle X_1,\dots,X_n,X_1^*,\dots,X_n^*\rangle \to \mathcal A
\end{align*}
denote the unital $*$-homomorphism determined by $\operatorname{ev}_a(X_i)=a_i$ and $\operatorname{ev}_a(X_i^*)=a_i^*$ for each $i \in \{1,\dots,n\}$. Thus, for every noncommutative $*$-polynomial $P$, the evaluated element is
\begin{align*}
\operatorname{ev}_a(P)=P(a_1,\dots,a_n,a_1^*,\dots,a_n^*) \in \mathcal A.
\end{align*}
By definition of the joint $*$-law,
\begin{align*}
\mu_{a_1,\dots,a_n}(P)=\varphi(\operatorname{ev}_a(P)).
\end{align*}
[/step]
[step:Use state normalization to evaluate the unit]
Because $\operatorname{ev}_a$ is unital, it sends the unit polynomial $1$ to $1_{\mathcal A}$. Therefore, by the definition of $\mu_{a_1,\dots,a_n}$ and the normalization of the state $\varphi$,
\begin{align*}
\mu_{a_1,\dots,a_n}(1)=\varphi(\operatorname{ev}_a(1))=\varphi(1_{\mathcal A})=1.
\end{align*}
[/step]
[step:Convert a polynomial square into an algebraic square after evaluation]
Fix $P \in \mathbb C\langle X_1,\dots,X_n,X_1^*,\dots,X_n^*\rangle$, and define
\begin{align*}
b := \operatorname{ev}_a(P) \in \mathcal A.
\end{align*}
Since $\operatorname{ev}_a$ is a $*$-homomorphism, it preserves products and involution. Hence
\begin{align*}
\operatorname{ev}_a(P^*P)=\operatorname{ev}_a(P^*)\operatorname{ev}_a(P)=\operatorname{ev}_a(P)^*\operatorname{ev}_a(P)=b^*b.
\end{align*}
[guided]
Fix a noncommutative $*$-polynomial
\begin{align*}
P \in \mathbb C\langle X_1,\dots,X_n,X_1^*,\dots,X_n^*\rangle.
\end{align*}
We define the evaluated algebra element
\begin{align*}
b := \operatorname{ev}_a(P) \in \mathcal A.
\end{align*}
The point of introducing $b$ is that the positivity axiom for a state is stated for elements of $\mathcal A$, not directly for formal polynomials. We therefore have to translate the formal polynomial square $P^*P$ into an actual square inside $\mathcal A$.
The map
\begin{align*}
\operatorname{ev}_a: \mathbb C\langle X_1,\dots,X_n,X_1^*,\dots,X_n^*\rangle \to \mathcal A
\end{align*}
is a unital $*$-homomorphism by construction: it sends each formal generator $X_i$ to $a_i$, sends each formal adjoint generator $X_i^*$ to $a_i^*$, preserves multiplication, and preserves the involution. Applying these two preservation properties to $P^*P$ gives
\begin{align*}
\operatorname{ev}_a(P^*P)=\operatorname{ev}_a(P^*)\operatorname{ev}_a(P).
\end{align*}
Because $\operatorname{ev}_a$ preserves the involution,
\begin{align*}
\operatorname{ev}_a(P^*)=\operatorname{ev}_a(P)^*.
\end{align*}
Substituting the definition $b=\operatorname{ev}_a(P)$, we obtain
\begin{align*}
\operatorname{ev}_a(P^*P)=b^*b.
\end{align*}
Thus the polynomial expression $P^*P$ evaluates exactly to the positive square $b^*b$ in the $*$-algebra $\mathcal A$.
[/guided]
[/step]
[step:Apply positivity of the state to the evaluated square]
By definition of the joint $*$-law and by the identity from the previous step,
\begin{align*}
\mu_{a_1,\dots,a_n}(P^*P)=\varphi(\operatorname{ev}_a(P^*P))=\varphi(b^*b).
\end{align*}
Since $\varphi$ is a state on $\mathcal A$, its positivity axiom gives $\varphi(c^*c)\geq 0$ for every $c \in \mathcal A$. Applying this with $c=b$ gives
\begin{align*}
\varphi(b^*b)\geq 0.
\end{align*}
Therefore
\begin{align*}
\mu_{a_1,\dots,a_n}(P^*P)\geq 0.
\end{align*}
Because $P$ was arbitrary, the inequality holds for every noncommutative $*$-polynomial $P$.
[/step]
