[proofplan]
The proof is an unwinding of the definition of finite biproduct data in an additive category. In the forward direction, a finite biproduct comes equipped by definition with product projections, coproduct injections, and the Kronecker-delta compatibility identities. In the reverse direction, the assumed product and coproduct universal properties, together with those same compatibility identities, are exactly the data required for a finite biproduct diagram.
[/proofplan]
[step:Unpack the finite biproduct condition]
We use the standard definition of a finite biproduct in an additive category: a triple $(A,(\iota_i)_{i=1}^n,(\pi_i)_{i=1}^n)$ is a finite biproduct of $A_1,\ldots,A_n$ precisely when $(A,(\pi_i)_{i=1}^n)$ is a product of $A_1,\ldots,A_n$, $(A,(\iota_i)_{i=1}^n)$ is a coproduct of $A_1,\ldots,A_n$, and the compatibility identities
\begin{align*}
\pi_i \circ \iota_j = \delta_{ij}
\end{align*}
hold for every $i,j \in \{1,\ldots,n\}$.
Here $\delta_{ij}: A_j \to A_i$ denotes the identity morphism $\operatorname{id}_{A_i}: A_i \to A_i$ when $i=j$, and the zero morphism $0_{A_j,A_i}: A_j \to A_i$ when $i \ne j$. The zero morphisms exist because $\mathcal{C}$ is additive.
[/step]
[step:Derive the product, coproduct, and Kronecker delta identities from a biproduct]
Assume that $(A,(\iota_i)_{i=1}^n,(\pi_i)_{i=1}^n)$ is a finite biproduct of $A_1,\ldots,A_n$. By the definition recalled above, the projections $\pi_i: A \to A_i$ exhibit $A$ as a product of $A_1,\ldots,A_n$, the injections $\iota_i: A_i \to A$ exhibit $A$ as a coproduct of $A_1,\ldots,A_n$, and the identities
\begin{align*}
\pi_i \circ \iota_j = \delta_{ij}
\end{align*}
hold for all $i,j \in \{1,\ldots,n\}$. This proves the forward implication.
[/step]
[step:Verify that the stated data satisfy the definition of a biproduct]
Conversely, assume that $(A,(\pi_i)_{i=1}^n)$ is a product of $A_1,\ldots,A_n$, that $(A,(\iota_i)_{i=1}^n)$ is a coproduct of $A_1,\ldots,A_n$, and that
\begin{align*}
\pi_i \circ \iota_j = \delta_{ij}
\end{align*}
for every $i,j \in \{1,\ldots,n\}$. These are exactly the three requirements in the definition of a finite biproduct diagram in an additive category. Therefore $(A,(\iota_i)_{i=1}^n,(\pi_i)_{i=1}^n)$ is a finite biproduct of $A_1,\ldots,A_n$.
[guided]
We prove the reverse implication by checking each part of the definition, rather than constructing any new object or any new morphisms. The object $A$ and the morphisms
\begin{align*}
\iota_i: A_i \to A
\end{align*}
and
\begin{align*}
\pi_i: A \to A_i
\end{align*}
are already part of the hypotheses.
First, the hypothesis that $(A,(\pi_i)_{i=1}^n)$ is a product says precisely that the morphisms $\pi_i: A \to A_i$ are the product projections for the family $A_1,\ldots,A_n$. Second, the hypothesis that $(A,(\iota_i)_{i=1}^n)$ is a coproduct says precisely that the morphisms $\iota_i: A_i \to A$ are the coproduct injections for the same family. Third, the displayed identity
\begin{align*}
\pi_i \circ \iota_j = \delta_{ij}
\end{align*}
states the required compatibility between projections and injections: if $i=j$, then the composite $A_i \xrightarrow{\iota_i} A \xrightarrow{\pi_i} A_i$ is $\operatorname{id}_{A_i}$, while if $i \ne j$, then the composite $A_j \xrightarrow{\iota_j} A \xrightarrow{\pi_i} A_i$ is the zero morphism $0_{A_j,A_i}$.
The point of this compatibility condition is that it identifies the product and coproduct structures as the same finite additive decomposition, rather than two unrelated universal structures carried by the same object. Since the assumed data satisfy the product condition, the coproduct condition, and the Kronecker-delta compatibility condition, they satisfy exactly the definition of a finite biproduct. Hence $(A,(\iota_i)_{i=1}^n,(\pi_i)_{i=1}^n)$ is a finite biproduct of $A_1,\ldots,A_n$.
[/guided]
[/step]
[step:Conclude the equivalence]
The forward implication and the reverse implication together prove that the given triple is a finite biproduct of $A_1,\ldots,A_n$ if and only if the stated product, coproduct, and Kronecker-delta conditions hold.
[/step]
