[proofplan] We prove existence by induction on the length of the finite family. The empty family is represented by a zero object, the one-object family by the object itself, and the two-object case is part of the definition of an additive category. For the inductive step, we append $A_n$ to an already constructed biproduct of $A_1,\dots,A_{n-1}$ and use the binary biproduct structure. Uniqueness is proved directly from the biproduct equations by writing the only possible comparison morphisms as finite matrix sums. [/proofplan] [step:Handle the empty and one-object families] Because $\mathcal C$ is additive, it has a zero object. For $n=0$, choose such a zero object $0_{\mathcal C}$ as $B$. There are no structure morphisms, and the empty sum condition is precisely the identity condition on a zero object. For $n=1$, choose $B=A_1$, define \begin{align*} i_1 := \operatorname{id}_{A_1}: A_1 \to A_1, \qquad p_1 := \operatorname{id}_{A_1}: A_1 \to A_1. \end{align*} Then $p_1 i_1=\operatorname{id}_{A_1}$ and \begin{align*} \sum_{j=1}^{1} i_j p_j = i_1 p_1 = \operatorname{id}_{A_1}. \end{align*} Thus the required object exists for $n=0$ and $n=1$. [/step] [step:Construct the finite biproduct inductively from binary biproducts] Assume that $n \geq 2$ and that a biproduct of $A_1,\dots,A_{n-1}$ has already been constructed. Denote it by $B_{n-1}$, with structure morphisms \begin{align*} i_j^{n-1}: A_j \to B_{n-1}, \qquad p_j^{n-1}: B_{n-1} \to A_j \end{align*} for $1 \leq j \leq n-1$, satisfying \begin{align*} p_j^{n-1} i_k^{n-1} = \begin{cases} \operatorname{id}_{A_j}, & j=k,\\ 0, & j \neq k, \end{cases} \qquad \sum_{j=1}^{n-1} i_j^{n-1}p_j^{n-1} = \operatorname{id}_{B_{n-1}}. \end{align*} Since $\mathcal C$ is additive, it has binary biproducts. Choose a binary biproduct \begin{align*} B := B_{n-1} \oplus A_n \end{align*} with structure morphisms \begin{align*} u: B_{n-1} \to B, \qquad q: B \to B_{n-1}, \qquad i_n: A_n \to B, \qquad p_n: B \to A_n, \end{align*} satisfying \begin{align*} q u = \operatorname{id}_{B_{n-1}}, \qquad p_n i_n = \operatorname{id}_{A_n}, \qquad q i_n = 0, \qquad p_n u = 0, \qquad u q + i_n p_n = \operatorname{id}_B. \end{align*} For $1 \leq j \leq n-1$, define \begin{align*} i_j: A_j \to B, \qquad i_j := u i_j^{n-1}, \end{align*} and \begin{align*} p_j: B \to A_j, \qquad p_j := p_j^{n-1} q. \end{align*} Keep the already named maps $i_n: A_n \to B$ and $p_n: B \to A_n$ for the last object. We verify the biproduct equations. If $1 \leq j,k \leq n-1$, then \begin{align*} p_j i_k = p_j^{n-1} q u i_k^{n-1} = p_j^{n-1} i_k^{n-1} = \begin{cases} \operatorname{id}_{A_j}, & j=k,\\ 0, & j \neq k. \end{cases} \end{align*} If $1 \leq j \leq n-1$, then \begin{align*} p_j i_n = p_j^{n-1} q i_n = p_j^{n-1} 0 = 0, \end{align*} and \begin{align*} p_n i_j = p_n u i_j^{n-1} = 0 i_j^{n-1} = 0. \end{align*} Finally $p_n i_n=\operatorname{id}_{A_n}$ by the binary biproduct equations. For the identity decomposition, use the inductive identity on $B_{n-1}$ and the binary identity on $B$: \begin{align*} \sum_{j=1}^{n} i_j p_j &= \sum_{j=1}^{n-1} u i_j^{n-1} p_j^{n-1} q + i_n p_n \\ &= u\left(\sum_{j=1}^{n-1} i_j^{n-1} p_j^{n-1}\right)q + i_n p_n \\ &= u \operatorname{id}_{B_{n-1}} q + i_n p_n \\ &= u q + i_n p_n \\ &= \operatorname{id}_B. \end{align*} Thus $B$ is a biproduct of $A_1,\dots,A_n$. By induction, such a finite biproduct exists for every $n \geq 0$. [/step] [step:Build the unique comparison isomorphism between two finite biproducts] Let $(B,i_j,p_j)$ and $(B',i'_j,p'_j)$ be two biproducts of $A_1,\dots,A_n$. Define morphisms \begin{align*} \varphi: B \to B', \qquad \varphi := \sum_{j=1}^n i'_j p_j, \end{align*} and \begin{align*} \psi: B' \to B, \qquad \psi := \sum_{j=1}^n i_j p'_j. \end{align*} These finite sums are defined because each hom-set in an additive category is an abelian group and composition is bilinear. We compute their composites. Using bilinearity of composition and the relations $p'_j i'_k=\delta_{jk}\operatorname{id}_{A_j}$, where $\delta_{jk}$ denotes the Kronecker delta, we get \begin{align*} \varphi\psi &= \left(\sum_{j=1}^n i'_j p_j\right) \left(\sum_{k=1}^n i_k p'_k\right) \\ &= \sum_{j=1}^n\sum_{k=1}^n i'_j p_j i_k p'_k \\ &= \sum_{j=1}^n i'_j p'_j \\ &= \operatorname{id}_{B'}. \end{align*} Similarly, using $p_j i_k=\delta_{jk}\operatorname{id}_{A_j}$, \begin{align*} \psi\varphi &= \left(\sum_{j=1}^n i_j p'_j\right) \left(\sum_{k=1}^n i'_k p_k\right) \\ &= \sum_{j=1}^n\sum_{k=1}^n i_j p'_j i'_k p_k \\ &= \sum_{j=1}^n i_j p_j \\ &= \operatorname{id}_B. \end{align*} Therefore $\varphi$ is an isomorphism with inverse $\psi$. [/step] [step:Verify compatibility and uniqueness of the comparison isomorphism] For each $1 \leq k \leq n$, the morphism $\varphi$ satisfies \begin{align*} \varphi i_k = \left(\sum_{j=1}^n i'_j p_j\right)i_k = \sum_{j=1}^n i'_j p_j i_k = i'_k. \end{align*} Likewise, \begin{align*} p'_k \varphi = p'_k\left(\sum_{j=1}^n i'_j p_j\right) = \sum_{j=1}^n p'_k i'_j p_j = p_k. \end{align*} It remains to prove uniqueness. Let $\theta: B \to B'$ be any morphism satisfying $\theta i_j=i'_j$ for every $1 \leq j \leq n$. Since $\sum_{j=1}^n i_j p_j=\operatorname{id}_B$, we have \begin{align*} \theta = \theta \operatorname{id}_B = \theta\left(\sum_{j=1}^n i_j p_j\right) = \sum_{j=1}^n \theta i_j p_j = \sum_{j=1}^n i'_j p_j = \varphi. \end{align*} Thus there is at most one morphism compatible with all inclusions, and the morphism $\varphi$ constructed above is that unique morphism. Since $\varphi$ is an isomorphism and also satisfies $p'_j\varphi=p_j$ for all $j$, the finite biproduct is unique up to unique isomorphism compatible with all inclusions and projections. [/step]