The opposite Deligne product is the category of finite bimodules

Use the supplied finite-dimensional unital $k$-algebras $R,S$ and $k$-linear equivalences of [F1] $\mathcal{A}\simeq R\text{-}\mathrm{m}\mathrm{o}\mathrm{d}$, $\mathcal{B}\simeq S\text{-}\mathrm{m}\mathrm{o}\mathrm{d}$ (Equivalence, quasi-inverse, and adjoint equivalence of categories, Algebras over a commutative ring, central structure maps, and algebra homomorphisms, Finite-dimensional vector space, and its dimension ${\dim }_{F}V$; infinite-dimensional means having no finite basis). The $k$-dual $X^{\ast }={\mathrm{Hom}}_k(X,k)$ with the right $R$-action $(\lambda \cdot a)(x)=\lambda (ax)$, equivalently the left $R^{\mathrm{o}\mathrm{p}}$-action $a\cdot \lambda :=\lambda \cdot a$, is a contravariant exact equivalence to $R^{\mathrm{o}\mathrm{p}}\text{-}\mathrm{m}\mathrm{o}\mathrm{d}$ [F2] (Linear functionals and the algebraic dual $V^{\ast }=\mathcal{L}(V,F)$), so it identifies ${\mathcal{A}}^{\mathrm{o}\mathrm{p}}$ with $R^{\mathrm{o}\mathrm{p}}\text{-}\mathrm{m}\mathrm{o}\mathrm{d}$ (Opposite category ${\mathcal{C}}^{\mathrm{o}\mathrm{p}}$, The opposite ring $R^{\mathrm{o}\mathrm{p}}$); $R^{\mathrm{o}\mathrm{p}}\text{-}\mathrm{m}\mathrm{o}\mathrm{d}$ and $S\text{-}\mathrm{m}\mathrm{o}\mathrm{d}$ are finite $k$-linear abelian categories [F6] (Abelian category, k-linear categories and k-linear functors).

By [F3] applied to the finite-dimensional algebras $R^{\mathrm{o}\mathrm{p}}$ and $S$, the category $(R^{\mathrm{o}\mathrm{p}}{\otimes }_{k}S)\text{-}\mathrm{m}\mathrm{o}\mathrm{d}$ with its tensor bifunctor is a Deligne product of $R^{\mathrm{o}\mathrm{p}}\text{-}\mathrm{m}\mathrm{o}\mathrm{d}$ and $S\text{-}\mathrm{m}\mathrm{o}\mathrm{d}$, so transporting along step 1.1 identifies ${\mathcal{A}}^{\mathrm{o}\mathrm{p}}⊠\mathcal{B}$ with $(R^{\mathrm{o}\mathrm{p}}{\otimes }_{k}S)\text{-}\mathrm{m}\mathrm{o}\mathrm{d}$. A left module over $R^{\mathrm{o}\mathrm{p}}{\otimes }_{k}S$ is a $k$-vector space with commuting left $R^{\mathrm{o}\mathrm{p}}$- and left $S$-actions [F4], that is, a $k$-vector space with a right $R$-action and a left $S$-action that commute, i.e. a finite-dimensional $(S,R)$-bimodule ($(S,R)$-bimodules and commuting left and right scalar actions, Unital left and right modules over a ring; unqualified module means left module, Vector space over a field, Modules over a ring form an abelian category); under the equivalences of step 1.1 this is exactly the category $(\mathcal{B},\mathcal{A})\text{-}\mathrm{b}\mathrm{i}\mathrm{m}\mathrm{o}\mathrm{d}$ of finite-dimensional $(\mathcal{B},\mathcal{A})$-bimodules, so ${\mathcal{A}}^{\mathrm{o}\mathrm{p}}⊠\mathcal{B}\simeq (\mathcal{B},\mathcal{A})\text{-}\mathrm{b}\mathrm{i}\mathrm{m}\mathrm{o}\mathrm{d}$ as $k$-linear categories.

The universal bifunctor of ${\mathcal{A}}^{\mathrm{o}\mathrm{p}}⊠\mathcal{B}$ is the transport of the tensor bifunctor of $R^{\mathrm{o}\mathrm{p}}\text{-}\mathrm{m}\mathrm{o}\mathrm{d}\times S\text{-}\mathrm{m}\mathrm{o}\mathrm{d}$, so on the external object $\bar{a}⊠b$ it sends $(a,b)$ to $a^{\ast }{\otimes }_{k}b$, where $a^{\ast }={\mathrm{Hom}}_k(a,k)$ carries the induced right $\mathcal{A}$-action and $b$ its left $\mathcal{B}$-action [F2, F4, F5]. The symmetry of the tensor product over the field, induced by the balanced map $(x,y)\mapsto y\otimes x$ and unique factorization through the tensor product [F5], is a natural isomorphism $a^{\ast }{\otimes }_{k}b\cong b{\otimes }_k{a}^{\ast }$ compatible with the two actions (Module homomorphisms induce tensor-product homomorphisms functorially, Linear functionals and the algebraic dual $V^{\ast }=\mathcal{L}(V,F)$), so the equivalence carries $\bar{a}⊠b$ to $b{\otimes }_k{a}^{\ast }$ with those actions, as asserted.

The tensor product of finite-dimensional $k$-vector spaces is exact in each variable: if $f:Y\to Y^{\mathrm{\prime }}$ is injective, then a $k$-linear retraction $r$ of $f$ exists because a basis of the image of $f$ extends to a basis of the finite-dimensional space $Y^{\mathrm{\prime }}$ (Finite-dimensional vector space, and its dimension ${\dim }_{F}V$; infinite-dimensional means having no finite basis), and $(1\otimes r)(1\otimes f)=1$ by functoriality [F5], so $1\otimes f$ is injective; right exactness in each variable holds by F3, so $⊠$ is also left exact in each variable (Left exact and right exact functors). Passing to opposites, $((R^{\mathrm{o}\mathrm{p}}{\otimes }_{k}S)\text{-}\mathrm{m}\mathrm{o}\mathrm{d}{)}^{\mathrm{o}\mathrm{p}}\simeq (R{\otimes }_k{S}^{\mathrm{o}\mathrm{p}})\text{-}\mathrm{m}\mathrm{o}\mathrm{d}$, via the finite contravariant duality of [F2] for the algebra $R^{\mathrm{o}\mathrm{p}}{\otimes }_{k}S$, followed by the algebra isomorphism $(R^{\mathrm{o}\mathrm{p}}{\otimes }_{k}S{)}^{\mathrm{o}\mathrm{p}}\cong R{\otimes }_k{S}^{\mathrm{o}\mathrm{p}}$, checked on elementary tensors [F4, F7]; by [F3] the category $(R{\otimes }_k{S}^{\mathrm{o}\mathrm{p}})\text{-}\mathrm{m}\mathrm{o}\mathrm{d}$ with its tensor bifunctor is a Deligne product of $R\text{-}\mathrm{m}\mathrm{o}\mathrm{d}$ and $S^{\mathrm{o}\mathrm{p}}\text{-}\mathrm{m}\mathrm{o}\mathrm{d}$, so transporting along step 1.1 gives the canonical equivalence $({\mathcal{A}}^{\mathrm{o}\mathrm{p}}⊠\mathcal{B}{)}^{\mathrm{o}\mathrm{p}}\simeq \mathcal{A}⊠{\mathcal{B}}^{\mathrm{o}\mathrm{p}}$.

The universal property dualises: a $k$-linear functor $G$ out of ${\mathcal{A}}^{\mathrm{o}\mathrm{p}}⊠\mathcal{B}$ is left exact exactly when its opposite functor out of $({\mathcal{A}}^{\mathrm{o}\mathrm{p}}⊠\mathcal{B}{)}^{\mathrm{o}\mathrm{p}}$ is right exact [F7], and step 3.2 identifies that opposite source with $\mathcal{A}⊠{\mathcal{B}}^{\mathrm{o}\mathrm{p}}$, where [F3] is the equivalence ${\mathrm{Rex}}_k(\mathcal{A}⊠{\mathcal{B}}^{\mathrm{o}\mathrm{p}},{\mathcal{E}}^{\mathrm{o}\mathrm{p}})\simeq {\mathrm{Rex}}_{k,k}(\mathcal{A}\times {\mathcal{B}}^{\mathrm{o}\mathrm{p}},{\mathcal{E}}^{\mathrm{o}\mathrm{p}})$ for every $k$-linear abelian $\mathcal{E}$; applying the same duality to the bifunctors turns right exactness in each variable on $\mathcal{A}\times {\mathcal{B}}^{\mathrm{o}\mathrm{p}}$ into left exactness in each variable on ${\mathcal{A}}^{\mathrm{o}\mathrm{p}}\times \mathcal{B}$ [F7], so restriction along $⊠$ induces an equivalence ${\mathrm{Lex}}_k({\mathcal{A}}^{\mathrm{o}\mathrm{p}}⊠\mathcal{B},\mathcal{E})\simeq {\mathrm{Lex}}_{k,k}({\mathcal{A}}^{\mathrm{o}\mathrm{p}}\times \mathcal{B},\mathcal{E})$ as well (Equivalence, quasi-inverse, and adjoint equivalence of categories, Functor category $[\mathcal{C},\mathcal{D}]$, Natural transformation and its components); the left exact external-tensor formula of the categorical Eilenberg–Watts triangle on this page is therefore an instance of the universal property in its dual form. A second choice of module models is related to the first by a $k$-linear equivalence [F1], and conjugating by it identifies the transported equivalences together with their universal bifunctors, so the construction is well defined up to an equivalence respecting the universal bifunctors; no commutativity of the algebras and no further choice beyond the supplied module equivalences and the existence theorem's AC-dependent data is used.