 be a pair of transfer mappings. For simplicity, we assume that the sets of worlds \(W_m\) of \(m\in {{\cal M}}_1\) are pairwise disjoints, and the same holds for \({{\cal M}}_2\). Given \(m\in {{\cal M}}_1 \cup {{\cal M}}_2\), \(w\in W_m\) and a formula \(\varphi\) in the fibred language, the satisfaction of \(\varphi\) in \(\langle h_1,h_2,m,w\rangle\), denoted by \(\langle h_1,h_2,m,w\rangle\Vdash \varphi\), is defined recursively as usual whenever the main connective of \(\varphi\) is Boolean (\(\neg\) or \(\to\)), or when \(\varphi\) is atomic. For the modalities, satisfaction is defined as follows: suppose (without loss of generality) that \(m \in {{\cal M}}_1\), and let \(h_1(w)=\langle m_2,w_2\rangle\), with \(m=\langle W_m,R_m,V_m\rangle\) and \(m_2=\langle W_{m_2},R_{m_2},V_{m_2}\rangle\). Then: