 In other words, when \(\Box_{2}\) needs to be evaluated, the transfer mapping uses current evaluation point \(w_1\) to obtain a pointed semantic model \(h_1(w_1) = (M_2, w_2)\) where the modality will be evaluated. When the analogous situation arises, facing the evaluation of \(\Box_{1}\) on a tuple \(\langle h_1, h_2, M_2, w_2 \rangle\), it is the turn of the second transfer function \(h_2\) to make its appearance, taking us then from \(\langle h_1, h_2, M_2, w_2 \rangle \Vdash \Box_{2}\varphi\) to \(\langle h_1, h_2, h_2(w_2) \rangle \Vdash \Box_{2}\varphi\).