Generic coordinate reals for finite-function forcing (source code)

= Generic coordinate reals for finite-function forcing
{title2=$c_\xi(n)=(\bigcup G)(\xi,n)$}

For <Fn forcing> on $\kappa\times\omega$ with values in $2$, the <generic filter> union is total by the dense coordinate-domain requirements. For each pair of distinct rows, the <set> of conditions giving them opposite bits at some column is dense: choose a column untouched in both finite rows. Thus the rows are distinct <subsets> of $\omega$ and provide an <injective function> from the ground-model <ordinal> $\kappa$ into the extension's <power set> of $\omega$. This construction alone does not prove preservation of its ground-model <cardinal number> status.