composition of forcing notions

Suppose $P$ is a forcing notion in $\\mathfrak{M}$ and $\\hat{Q}$ is some $P$ -name such that $\\Vdash_{P}\\hat{Q}$ 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]$ .