[proofplan]
We use the central idempotents $e_R=(1_R,0_S)$ and $e_S=(0_R,1_S)$ in $R\times S$ to decompose modules over the product ring into their $R$- and $S$-parts. This decomposition identifies finitely generated projective $(R\times S)$-modules with pairs consisting of a finitely generated projective $R$-module and a finitely generated projective $S$-module, compatibly with direct sums. Hence it gives an isomorphism of the commutative monoids $V(R\times S)\cong V(R)\times V(S)$, and applying the universal property of group completion gives the asserted isomorphism on $K_0$.
[/proofplan]
[step:Decompose modules over $R\times S$ using the two product idempotents]
Let $A:=R\times S$, and let
\begin{align*}
e_R:=(1_R,0_S)\in A
\end{align*}
and
\begin{align*}
e_S:=(0_R,1_S)\in A.
\end{align*}
Then $e_R^2=e_R$, $e_S^2=e_S$, $e_Re_S=0$, and $e_R+e_S=1_A$.
Let $P$ be a left $A$-module. Define $e_RP:=\{e_Rp:p\in P\}$ and $e_SP:=\{e_Sp:p\in P\}$. The set $e_RP$ is a left $R$-module by
\begin{align*}
r\cdot x := (r,0_S)x
\end{align*}
for $r\in R$ and $x\in e_RP$. Similarly, $e_SP$ is a left $S$-module by
\begin{align*}
s\cdot y := (0_R,s)y
\end{align*}
for $s\in S$ and $y\in e_SP$.
For every $p\in P$ one has
\begin{align*}
p=1_Ap=(e_R+e_S)p=e_Rp+e_Sp.
\end{align*}
If $x\in e_RP\cap e_SP$, then $x=e_Rx$ and $x=e_Sx$, so
\begin{align*}
x=e_Rx=e_Re_Sx=0.
\end{align*}
Therefore
\begin{align*}
P=e_RP\oplus e_SP
\end{align*}
as abelian groups, and this decomposition is compatible with the $A$-module structure.
[/step]
[step:Identify the module category of the product with a product category]
Define a functor
\begin{align*}
\Phi:A\operatorname{-Mod}\to R\operatorname{-Mod}\times S\operatorname{-Mod}
\end{align*}
by
\begin{align*}
\Phi(P):=(e_RP,e_SP)
\end{align*}
on objects and, for an $A$-[linear map](/page/Linear%20Map) $f:P\to Q$, by
\begin{align*}
\Phi(f):=(f|_{e_RP},f|_{e_SP}).
\end{align*}
The restrictions are well-defined because, for $x\in e_RP$,
\begin{align*}
f(x)=f(e_Rx)=e_Rf(x)\in e_RQ,
\end{align*}
and the same argument applies to $e_SP$.
Conversely, define a functor
\begin{align*}
\Psi:R\operatorname{-Mod}\times S\operatorname{-Mod}\to A\operatorname{-Mod}
\end{align*}
by
\begin{align*}
\Psi(M,N):=M\oplus N
\end{align*}
with $A$-action
\begin{align*}
(r,s)\cdot(m,n):=(rm,sn)
\end{align*}
for $(r,s)\in A$ and $(m,n)\in M\oplus N$. On morphisms, $\Psi$ sends a pair $(g,h)$, where $g:M\to M'$ is $R$-linear and $h:N\to N'$ is $S$-linear, to the $A$-linear map
\begin{align*}
g\oplus h:M\oplus N\to M'\oplus N'
\end{align*}
given by
\begin{align*}
(g\oplus h)(m,n):=(g(m),h(n)).
\end{align*}
The decomposition in the previous step gives a natural $A$-linear isomorphism
\begin{align*}
P\to \Psi\Phi(P)
\end{align*}
sending $p\mapsto(e_Rp,e_Sp)$. Its inverse sends $(x,y)\mapsto x+y$. Also $\Phi\Psi(M,N)=(M,N)$ with the evident identifications. Thus this is the product-ring module equivalence described in [Projectives over a Product Ring][citetheorem:8635].
[guided]
The purpose of this step is to turn the algebra of the product ring into a categorical statement about modules. We define
\begin{align*}
\Phi:A\operatorname{-Mod}\to R\operatorname{-Mod}\times S\operatorname{-Mod}
\end{align*}
by
\begin{align*}
\Phi(P):=(e_RP,e_SP).
\end{align*}
If $f:P\to Q$ is $A$-linear, then $f$ respects the two summands because $A$-linearity gives
\begin{align*}
f(e_Rx)=e_Rf(x)
\end{align*}
for every $x\in P$, and similarly with $e_S$. Hence $\Phi(f)$ is the pair of restrictions
\begin{align*}
\Phi(f):=(f|_{e_RP},f|_{e_SP}).
\end{align*}
Now we construct the inverse direction. Given a left $R$-module $M$ and a left $S$-module $N$, define
\begin{align*}
\Psi(M,N):=M\oplus N
\end{align*}
as an abelian group, with left $A=R\times S$ action
\begin{align*}
(r,s)\cdot(m,n):=(rm,sn).
\end{align*}
This is an $A$-module because multiplication in $R\times S$ is componentwise. If $(r,s),(r',s')\in A$ and $(m,n)\in M\oplus N$, then
\begin{align*}
(r,s)\cdot((r',s')\cdot(m,n))=(r,s)\cdot(r'm,s'n)=(rr'm,ss'n).
\end{align*}
This equals
\begin{align*}
((r,s)(r',s'))\cdot(m,n),
\end{align*}
and the identity element $(1_R,1_S)$ acts as the identity.
For a module $P$ over $A$, the map
\begin{align*}
P\to e_RP\oplus e_SP
\end{align*}
defined by
\begin{align*}
p\mapsto(e_Rp,e_Sp)
\end{align*}
is $A$-linear. Its inverse is
\begin{align*}
e_RP\oplus e_SP\to P
\end{align*}
given by
\begin{align*}
(x,y)\mapsto x+y.
\end{align*}
The inverse property follows from $p=e_Rp+e_Sp$ and from the fact that $x=e_Rx$ and $y=e_Sy$ for $x\in e_RP$ and $y\in e_SP$. Thus the two constructions are mutually inverse up to natural isomorphism. This is precisely the equivalence stated in [Projectives over a Product Ring][citetheorem:8635].
[/guided]
[/step]
[step:Restrict the equivalence to finitely generated projective modules]
We verify that the preceding equivalence restricts to finitely generated projective modules.
First, suppose $P$ is a finitely generated projective left $A$-module. Since $P$ is finitely generated, there is an integer $n\ge 0$ and a surjective $A$-linear map
\begin{align*}
A^n\to P.
\end{align*}
Applying $\Phi$ gives surjective maps
\begin{align*}
R^n\to e_RP
\end{align*}
and
\begin{align*}
S^n\to e_SP,
\end{align*}
so $e_RP$ and $e_SP$ are finitely generated. Since $P$ is projective, the surjection $A^n\to P$ splits. Hence there exists a left $A$-module $Q$ such that
\begin{align*}
A^n\cong P\oplus Q.
\end{align*}
Set $m:=n$. Applying $\Phi$ gives
\begin{align*}
e_RP\oplus e_RQ\cong R^m
\end{align*}
and
\begin{align*}
e_SP\oplus e_SQ\cong S^m.
\end{align*}
Thus $e_RP$ is projective over $R$ and $e_SP$ is projective over $S$.
Conversely, suppose $M$ is a finitely generated projective left $R$-module and $N$ is a finitely generated projective left $S$-module. Choose integers $m,n\ge 0$ and modules $M'$ over $R$ and $N'$ over $S$ such that
\begin{align*}
M\oplus M'\cong R^m
\end{align*}
and
\begin{align*}
N\oplus N'\cong S^n.
\end{align*}
Let $k:=\max(m,n)$. Replacing $M'$ by $M'\oplus R^{k-m}$ and $N'$ by $N'\oplus S^{k-n}$, we obtain isomorphisms
\begin{align*}
M\oplus M'\cong R^k
\end{align*}
and
\begin{align*}
N\oplus N'\cong S^k.
\end{align*}
Therefore
\begin{align*}
(M\oplus N)\oplus(M'\oplus N')\cong R^k\oplus S^k\cong A^k
\end{align*}
as left $A$-modules. Hence $\Psi(M,N)=M\oplus N$ is projective over $A$. It is finitely generated because finite generating sets for $M$ and $N$ together generate $M\oplus N$ over $A$.
[/step]
[step:Construct the monoid isomorphism on $V$]
For a unital ring $T$, let $V(T)$ denote the commutative monoid of isomorphism classes $[P]$ of finitely generated projective left $T$-modules, with operation
\begin{align*}
[P]+[Q]:=[P\oplus Q].
\end{align*}
The operation is a commutative monoid operation by [V Is A Commutative Monoid][citetheorem:8629].
Define a map of commutative monoids
\begin{align*}
\theta:V(A)\to V(R)\times V(S)
\end{align*}
by
\begin{align*}
\theta([P]):=([e_RP],[e_SP]).
\end{align*}
This is well-defined because isomorphic $A$-modules have isomorphic $R$- and $S$-components under $\Phi$. It is a monoid homomorphism because $\Phi$ preserves direct sums:
\begin{align*}
e_R(P\oplus Q)=e_RP\oplus e_RQ
\end{align*}
and
\begin{align*}
e_S(P\oplus Q)=e_SP\oplus e_SQ.
\end{align*}
Define
\begin{align*}
\eta:V(R)\times V(S)\to V(A)
\end{align*}
by
\begin{align*}
\eta([M],[N]):=[M\oplus N],
\end{align*}
where $M\oplus N$ is regarded as an $A$-module through $\Psi$. The equivalence above shows that $\theta\eta$ and $\eta\theta$ are identity maps. Therefore
\begin{align*}
V(R\times S)\cong V(R)\times V(S)
\end{align*}
as commutative monoids.
[/step]
[step:Apply group completion and identify the resulting product]
For any commutative monoid $M$, let $G(M)$ denote its group completion with universal monoid homomorphism
\begin{align*}
\iota_M:M\to G(M).
\end{align*}
By the defining convention for $K_0$,
\begin{align*}
K_0(T):=G(V(T))
\end{align*}
for every unital ring $T$.
The monoid isomorphism $\theta:V(A)\to V(R)\times V(S)$ induces an isomorphism
\begin{align*}
G(V(A))\cong G(V(R)\times V(S)).
\end{align*}
It remains to identify the group completion of the product monoid. By the [Universal Property of Group Completion][citetheorem:8633], for every abelian group $B$ and every monoid homomorphism
\begin{align*}
f:V(R)\times V(S)\to B,
\end{align*}
there is a unique [group homomorphism](/page/Group%20Homomorphism) from $G(V(R)\times V(S))$ to $B$ extending $f$. The product group $G(V(R))\times G(V(S))$, together with the monoid homomorphism
\begin{align*}
([M],[N])\mapsto(\iota_{V(R)}([M]),\iota_{V(S)}([N])),
\end{align*}
has the same universal property. Indeed, if $f:V(R)\times V(S)\to B$ is a monoid homomorphism, then
\begin{align*}
f(x,y)=f(x,0)+f(0,y)
\end{align*}
for all $x\in V(R)$ and $y\in V(S)$. Thus $f$ is determined by the two restricted monoid homomorphisms $x\mapsto f(x,0)$ and $y\mapsto f(0,y)$. These uniquely extend to group homomorphisms $u:G(V(R))\to B$ and $v:G(V(S))\to B$, and the corresponding group homomorphism $G(V(R))\times G(V(S))\to B$ is
\begin{align*}
(a,b)\mapsto u(a)+v(b).
\end{align*} Therefore
\begin{align*}
G(V(R)\times V(S))\cong G(V(R))\times G(V(S)).
\end{align*}
Combining the displayed isomorphisms gives
\begin{align*}
K_0(R\times S)\cong K_0(R)\times K_0(S).
\end{align*}
Let $e_{R'}:=(1_{R'},0_{S'})\in R'\times S'$ and $e_{S'}:=(0_{R'},1_{S'})\in R'\times S'$. Naturality follows because for unital ring homomorphisms $\alpha:R\to R'$ and $\beta:S\to S'$, the induced homomorphism
\begin{align*}
\alpha\times\beta:R\times S\to R'\times S'
\end{align*}
sends $e_R$ to $e_{R'}$ and $e_S$ to $e_{S'}$. Under the product-ring equivalence, extension of scalars admits the componentwise comparison isomorphism
\begin{align*}
(R'\times S')\otimes_{R\times S}P \cong (R'\otimes_R e_RP)\oplus(S'\otimes_S e_SP)
\end{align*}
given on pure tensors by
\begin{align*}
(r',s')\otimes p \mapsto (r'\otimes e_Rp, s'\otimes e_Sp).
\end{align*}
Its inverse sends $(r'\otimes x,s'\otimes y)$ to $(r',0_{S'})\otimes x+(0_{R'},s')\otimes y$. These formulas are balanced over $R\times S$ because $e_R$ and $e_S$ project onto the two factors, and they identify the $e_{R'}$- and $e_{S'}$-summands of the scalar extension with $R'\otimes_R e_RP$ and $S'\otimes_S e_SP$. Hence the product decomposition on $K_0$ commutes with the induced maps.
[/step]
