Suppose $P$ is a forcing notion in $\mathfrak{M}$ and $\hat{Q}$ is some $P$ name such that $\Vdash_P \hat{Q}$ texttt is a forcing notion.

Then take a set of $P$ names $Q$ such that given a $P$ name $\tilde{Q}$ of $Q$ $\Vdash_P \tilde{Q}=\hat{Q}$ (that is, no matter which generic subset $G$ of $P$ we force with, the names in $Q$ correspond precisely to the elements of $\hat{Q}[G]$ . We can define

$$P*Q=\{\langle p,\hat{q}\rangle \mid p\in P, \hat{q}\in Q\}$$

We can define a partial order on $P*Q$ such that $\langle p_1,\hat{q}_1\rangle\leq \langle p_2,\hat{q}_2\rangle$ iff $p_1\leq_P p_2$ and $p_1\Vdash \hat{q}_1\leq_{\hat{Q}} \hat{q}_2$ (A note on interpretation: $q_1$ and $q_2$ are $P$ names; this requires only that $\hat{q}_1\leq \hat{q}_2$ in generic subsets contain $p_1$ so in other generic subsets that fact could fail.)

Then $P*\hat{Q}$ is itself a forcing notion, and it can be shown that forcing by $P*\hat{Q}$ is equivalent to forcing first by $P$ and then by $\hat{Q}[G]$