Fusion paths give a basis of the fixed-boundary path space

For $n=0$, $T_0=b$ and [F4] gives $\mathrm{Hom}(c,b)=0$ when $c\cong ̸b$. If $c\cong b$, composition with the chosen isomorphism $u_{c,b}:c\to b$ identifies $\mathrm{End}(c)=\mathbb{C}{\mathrm{id}}_c$ with $\mathrm{Hom}(c,b)$, so the latter has basis $u_{c,b}$. This is exactly the typed empty-path convention of [F1]. For $n=1$, the path vectors are directly the chosen basis $B_{b,a}^c$ of $\mathrm{Hom}(c,b\otimes a)$, since the starting map is ${\mathrm{id}}_b$. This separately proves the positive-length base case without requiring the bases for isomorphic but unequal external objects to coincide.

Fix $n\ge 1$ and assume for every simple endpoint $x$ that the length-$n$ path composites form a basis of $\mathrm{Hom}(x,T_n)$.

By finite semisimplicity, the induction hypothesis decomposes $T_n\cong {⨁}_{x,\gamma }x$, with one summand for each length-$n$ path $\gamma$ ending at $x$. Here $x$ ranges once over the fixed simple representatives, even when the external endpoints are different isomorphic objects. For each such $x$, finite semisimplicity gives $x\otimes a\cong {⨁}_y{y}^{\oplus N_{xa}^y}$. Applying $\mathrm{Hom}(y,-)$, all nonisomorphic simple summands vanish and each of the $N_{xa}^y$ copies of $y$ contributes $\mathrm{End}(y)=\mathbb{C}{\mathrm{id}}_y$ by [F4]. Hence $\dim W_{x,a}^y=N_{xa}^y$ and the specified inclusion basis has exactly that many vectors.

Choose retractions $p_{x,\gamma }:T_n\to x$ dual to the path inclusions $\gamma :x\to T_n$ in step 2.1. They exist by taking any semisimple decomposition and changing its inclusion basis to the given basis for each simple $x$; the inverse basis matrix changes its retractions. Thus ${\sum }_{x,\gamma }\gamma p_{x,\gamma }={\mathrm{id}}_{T_n}$ and $p_{x,\gamma }\gamma \mathrm{\prime }$ is the appropriate Kronecker identity. Tensoring gives a direct-sum decomposition of $T_n\otimes a$ with inclusions $\gamma \otimes {\mathrm{id}}_a$ and retractions $p_{x,\gamma }\otimes {\mathrm{id}}_a$. Applying $\mathrm{Hom}(c,-)$ therefore gives the isomorphism ${⨁}_{x,\gamma }\mathrm{Hom}(c,x\otimes a)\to \mathrm{Hom}(c,T_{n+1})$ sending $(h_{x,\gamma })$ to ${\sum }_{x,\gamma }(\gamma \otimes {\mathrm{id}}_a)h_{x,\gamma }$. Its inverse applies each displayed retraction. Inserting the specified basis $B_{x,a}^c$ in each summand gives exactly the length-$(n+1)$ path composites of [F1], so they form a basis, including when the external $c$ differs from its representative.

For $n\ge 1$, step 3.1 shows that each admissible path contributes one basis vector for every tuple of vertex indices, hence contributes ${\prod }_{j=1}^n\dim W_{x_{j-1},a}^{x_j}={\prod }_{j=1}^n{N}_{x_{j-1}a}^{x_j}$ vectors. Summing over the finitely many internal simple labels gives the displayed dimension; every sum is finite because the category has finitely many simple isomorphism classes and $n$ is finite. Step 1.1 gives the separate $n=0$ count. Induction completes the basis proof and count.