Cohen coordinates are distinct and mutually generic

For fixed $(\xi ,n)$, conditions defining that bit are dense, so $c_{\xi }$ is total. For $\xi \mathrm{\ne }\eta$, below any condition choose a fresh $n$ and assign opposite bits at $(\xi ,n)$ and $(\eta ,n)$; this dense set proves $c_{\xi }\mathrm{\ne }{c}_{\eta }$.

Restriction is an order isomorphism $\mathrm{Add}(\omega ,\lambda )\cong \mathrm{Add}(\omega ,I)\times \mathrm{Add}(\omega ,J)$, with inverse union, so each projection is ground-model generic. Let $D={\dot{D}}_{G_I}$ be dense open in the second factor in $M[G_I]$. Choose $p\in G_I$ forcing that $\dot{D}$ is dense. Below $(p,1)$, pairs $(r,t)$ for which $r⊩\check{t}\in \dot{D}$ are dense: below any $(r,s)$, forced density supplies an extension $t\le s$ in $\dot{D}$, and one may strengthen $r$ to decide a witnessing ground-model $t$. Adjoining all pairs whose first coordinate is incompatible with $p$ makes this a ground-model dense subset of the full product. The product generic meets it, and directedness with $p\in G_I$ excludes the incompatible branch; its second coordinate is the actual $t\in G_J\cap D$. Thus $G_J$ is generic over $M[G_I]$, and symmetry gives the reverse direction. If $I$ or $J$ is empty, its factor is the one-condition forcing, its projection gives the unique filter, and the same statement is literal.

Evaluation of a product name can be performed successively in either coordinate, and the full generic is recovered as $G_I\times G_J$. The three extension models are therefore equal. No choice beyond the stated ZFC background is hidden in the coordinate construction.