Substitution of Noncommutative Polynomials into the Variables

Let $m,n\in\mathbb{N}$, where $\mathbb{N}$ is the set of natural numbers, let $W_{n}$ be the set of words in the letters $1,\dots,n$ with empty word $\varnothing$, and for $l\in\mathbb{N}$ let $\mathcal{P}_{l}=\mathbb{C}\langle x_{1},\dots,x_{l}\rangle$ be the set of noncommutative polynomials in $l$ variables, with the product, the unit $1$ and the monomials $x_{w}$ of that definition. Let $a=(a_{1},\dots,a_{n})$ be an $n$-tuple in $\mathcal{P}_{m}$.

1. (Products along a word)¶ For $w\in W_{n}$ the polynomial $a_{w}\in\mathcal{P}_{m}$ is defined by $a_{\varnothing}=1$ and, if $w$ has length $k\in\mathbb{N}$,

meaning the value at $k$ of the unique map $\pi:[k]\to\mathcal{P}_{m}$ with $\pi(1)=a_{w_{1}}$ and $\pi(i+1)=\pi(i)\,a_{w_{i+1}}$ whenever $i+1\in[k]$, given by Existence and Uniqueness of Iterates of a Binary Operation for the product of $\mathcal{P}_{m}$.

2. (Substitution)¶ The substitution of $a$ is the unique linear map $\sigma_{a}:\mathcal{P}_{n}\to\mathcal{P}_{m}$ with $\sigma_{a}(x_{w})=a_{w}$ for every $w\in W_{n}$, which exists and is unique by Noncommutative Polynomials Form a Unital Complex Algebra with Involution: Linear Extension from Monomials, Products, Adjoints and Self-Adjoint Parts §linear-extension. For $p\in\mathcal{P}_{n}$ one also writes $p(a)=\sigma_{a}(p)$ and calls it the polynomial obtained by substituting $a_{j}$ for $x_{j}$.