Finite ancilla amplification is a well-defined block map

Choose finite bases of $H$ and $K$, which exist by [F7] and are linearly independent by the basis definition; apply [F9] to obtain orthonormal bases $(u_{\alpha })$ and $(v_{\beta })$ with the same spans. By [F1]–[F3], $(u_{\alpha }\otimes e_j{)}_{\alpha ,j}$ and $(v_{\beta }\otimes e_j{)}_{\beta ,j}$ are orthonormal bases of $H\otimes R$ and $K\otimes R$. For each $j,\alpha$, uniquely expand $X(u_{\alpha }\otimes e_j)={\sum }_{i<r,\beta }{c}_{\beta i;\alpha j}{u}_{\beta }\otimes e_i$. Define $X_{ij}{u}_{\alpha }={\sum }_{\beta }{c}_{\beta i;\alpha j}{u}_{\beta }$ and extend linearly from the basis of $H$. Linearity of $X$ gives the required block formula on every $x\in H$. Any other family satisfying it has the same coefficients on every product-basis vector, hence each block agrees on the basis $u_{\alpha }$ and is equal.

On each product-basis vector $v_{\beta }\otimes e_j$, prescribe the image ${\sum }_i\mathrm{\Phi }(X_{ij})v_{\beta }\otimes e_i$. Since these product vectors are a basis, there exists a unique linear operator $Y$ on $K\otimes R$ with those values. By linearity this gives the displayed rule for all $y\in K$. Define ${\mathrm{\Phi }}^{(r)}(X)=Y$. Uniqueness of the blocks from step 1.1 and uniqueness of an operator from its values on a basis show that this definition is unambiguous.

For $X,X^{\mathrm{\prime }}\in \mathcal{L}(H\otimes R)$, their block families are respectively $[X_{ij}]$ and $[X_{ij}^{\mathrm{\prime }}]$. The defining action on the product basis shows that the blocks of $sX+t{X}^{\mathrm{\prime }}$ are $s{X}_{ij}+t{X}_{ij}^{\mathrm{\prime }}$ for any scalars $s,t\in \mathbb{C}$. Applying the linearity of $\mathrm{\Phi }$ from [F6] gives blocks $s\mathrm{\Phi }(X_{ij})+t\mathrm{\Phi }(X_{ij}^{\mathrm{\prime }})$, which are exactly the blocks of $s{\mathrm{\Phi }}^{(r)}(X)+t{\mathrm{\Phi }}^{(r)}(X^{\mathrm{\prime }})$. Equality on a basis yields ${\mathrm{\Phi }}^{(r)}(sX+t{X}^{\mathrm{\prime }})=s{\mathrm{\Phi }}^{(r)}(X)+t{\mathrm{\Phi }}^{(r)}(X^{\mathrm{\prime }})$. When $r=1$, identify $R={\mathbb{C}}^1$ with the tensor unit $\mathbb{C}$ by $1\mapsto e_0$, and define $u_H:H\to H\otimes R$ and $u_K:K\to K\otimes R$ by $u_{H}x=x\otimes e_0$ and $u_{K}y=y\otimes e_0$. These are the corresponding canonical unit identifications of [F8]. By [F3], they send the orthonormal bases chosen in step 1.1 to the corresponding product bases, and [F1]–[F2] show they preserve inner products; hence they are unitary. The sole block equations are $X{u}_H=u_H{X}_{00}$ and ${\mathrm{\Phi }}^{(1)}(X)u_K=u_K\mathrm{\Phi }(X_{00})$, so $X_{00}=u_H^{-1}X{u}_H$ and $u_K^{-1}{\mathrm{\Phi }}^{(1)}(X)u_K=\mathrm{\Phi }(X_{00})=\mathrm{\Phi }(u_H^{-1}X{u}_H)$. This is the original map under these identifications.