The algebraic 2-category Mod(C) is a fusion 2-category

Composition of module functors is ordinary functor composition with the composite action comparison; its module equation follows by substituting the two module equations. Identities have identity comparison. Horizontal and vertical composition of module-natural transformations are their ordinary compositions and obey interchange because horizontal composition is a functor on the functor categories. Each hom category is finite semisimple by [F1]. The zero module category and finite direct sums of module categories are obtained componentwise; inclusions and projections are module functors. Their biproduct equations hold componentwise, and composition preserves these sums since every functor is linear. Both adjoints and all separable-monad splittings exist by [F2].

To identify simple objects, write the simple objects of a module category as $m_a$. Join $a$ to $b$ when $m_b$ is a summand of $m_a\odot X$ for a simple $X\in \mathcal{C}$. Rigidity makes this an undirected graph. Its components are precisely action-stable full semisimple summands, so indecomposability is connectedness. A natural endomorphism of the identity acts on $m_a$ as $t_a{1}_{m_a}$, because the field is algebraically closed and simple endomorphism rings are finite dimensional. Module-naturality and naturality along each summand inclusion force $t_a=t_b$ along every edge. Conversely scalars constant on components define module-natural endomorphisms. Thus the endomorphism algebra of the identity is one copy of the field for every component. In the semisimple hom category from [F1], an object is simple exactly when its endomorphism algebra is the field: decompose it into simples, whose endomorphism algebras are the field, and use the resulting product of matrix algebras. Hence nonzero simple objects of $\mathrm{Mod}(\mathcal{C})$ are exactly indecomposable module categories. By [F3] their ranks are bounded and only finitely many action multiplicity arrays occur; [F4] gives finitely many module equivalence classes for each array. There are consequently finitely many simple-object equivalence classes.

The universal relative products from [F5] supply the tensor pseudofunctor, its composition and identity comparisons, unit $\mathcal{C}$, associator and unit equivalences, and their coherence modifications. Its proofs establish naturality, the pentagon and triangle and interchange on transformations, so this is a weak monoidal structure on the same $2$-category of step 1.1. Under [F1], the identity of the regular module is the simple unit of $\mathcal{C}$; therefore the tensor unit is simple. Every object admits a separable algebra presentation by [F7]. The orientation is essential: an $A$-$B$ bimodule $X$, regarded as $A\to B$ in the algebra bicategory, acts on left modules by $X{\otimes }_B-:{\mathrm{Mod}}^l(B)\to {\mathrm{Mod}}^l(A)$. Thus Eilenberg–Watts identifies $\mathrm{Mod}(\mathcal{C})$ with the $1$-morphism-opposite of that algebra bicategory. Composing these functors identifies composition with balanced tensor, by the common balanced trilinear universal property. The product construction in [F5], evaluated on free modules and extended to their separability retracts, identifies tensoring these functors with tensoring their bimodules using the positive middle braid. Consequently this identification is monoidal with the stated reversal of $1$-morphisms. Fact [F6] supplies both left and right object duals there, with separate negative and positive opposite algebras. Reversing $1$-morphisms interchanges evaluation and coevaluation, so a left dual becomes a right dual and conversely; its invertible cusp maps become the corresponding inverse comparisons. Therefore both duals transport to $\mathrm{Mod}(\mathcal{C})$ with all their required source, target and inverse equations.

Steps 1.1 and 2.1 establish every clause of finite semisimplicity; step 2.2 establishes weak monoidality, a simple unit, and both object duals. These are exactly the requirements in [F8]. Thus $\mathrm{Mod}(\mathcal{C})$ is a fusion $2$-category under the full stated hypotheses.