or \ell \in \{1,2\} let \bar L_\ell = \langle L_{\ell,i}:i < 4 \rangle be defined by:
\oplus_1 (a) \quad L_{\ell,0} = L_0,
{{}} (b) \quad L_{\ell,1} = L_1,
{{}} (c) \quad L_{\ell,2} = \{s \in L_{\mathbf m_\ell}:s \le_{\mathbf m_\ell} t for some t \in L_0\},
{{}} (d) \quad L_{\ell,3} = L_{\mathbf m_\ell}.
Clearly,
\oplus_2 (a) \quad (\mathbf m_\ell,\bar L_\ell) satisfies the assumptions of 1.24 hence,
{{}} (b) \quad {\mathbb P}_{\mathbf m_\ell}(L_{\ell,1}) \lessdot {\mathbb P}_{\mathbf m_\ell}(L_{\ell,3}) which means {\mathbb P}_{\mathbf m_\ell}(L_1) \lessdot {\mathbb P}_{\mathbf m_\ell} for \ell=1,2.
Why \oplus_2? Clearly it suffices to prove clause (a), so we just have to check clauses (*)(a)-(f) of 1.24.
Clause (*)(a):
By \oplus_1(d),L_{\ell,3} = L_{\mathbf m_\ell} hence is an initial segment of L_{\mathbf m_\ell} and by \oplus_1(c),L_{\ell,2} is an initial segment of L_{\mathbf m_\ell} which is L_{\ell,3} so L_{\ell,2} \subseteq L_{\ell,3}.
Clause (*)(b):
For the first statement, L_{\ell,1} \subseteq L_{\ell,3} is trivial by \oplus_1(d) + \oplus_1(b) + \boxdot(a),(b). The second statement says L_{\ell,0} = L_{\ell,1}
\cap L_{\ell,2}. Now L_{\ell,0} \subseteq L_{\ell,1} by \boxdot(a),(b) of the claim and \oplus_1(a),(b). Also L_{\ell,0}
\subseteq L_{\ell,2} holds by \oplus_1(c) (and \oplus_1(a)). Together L_{\ell,0} \subseteq L_{\ell,1} \cap L_{\ell,2}; to prove the inverse inclusion assume s \in L_{\ell,2} \cap L_{\ell,1}, so as s \in L_{\ell,2} by \oplus_1(c) there is t \in L_0 such that s
\le_{\mathbf m_\ell} t. But s \in L_{\ell,1} = L_1 so by \boxdot(c) of the claim we have s \in L_0 = L_{\ell,0} as promised.
Clause (*)(c):
Holds by condition \boxdot(c) of the claim.
Clause (*)(d):
By clause \boxdot(f) of the claim and \oplus_1(c),L_{\ell,2} is an initial segment of L_{\mathbf m_\ell}, hence by 1.13(e) we have {\mathbb P}_{\mathbf m_\ell}(L_{\ell,2}) \lessdot {\mathbb P}_{\mathbf m_\ell} = {\mathbb P}_{\mathbf m_\ell}(L_{\ell,3}). By \boxdot(e) \,
{\mathbb P}_{\mathbf m_0}(L_{\ell,0}) \lessdot {\mathbb P}_{\mathbf m_\ell}; so together as L_{\ell,0} \subseteq L_{\ell,2}, we have {\mathbb P}_{\mathbf m_\ell}(L_0) \lessdot {\mathbb P}_{\mathbf m_\ell}(L_{\ell,2}).
Clauses (*)(e),(f):
Hold by condition \boxdot(f) of the claim.
So \oplus_2 holds indeed. So now we deal with the other half.
Proof of: {\mathbb P}_{\mathbf m_1}(L_1) = {\mathbb P}_{\mathbf m_2}(L_1).
Let \langle s_\alpha:\alpha < \alpha(*)\rangle list L_1 \backslash L_0 such that s_\alpha \le_{L_{\mathbf m}} s_\beta \Rightarrow \alpha
\le \beta. This is possible as L_{\mathbf m_2} is well founded.
Now,
\oplus_3 for \ell=1,2 and \alpha \le \alpha(*) let \bar L^*_{\ell,\alpha} = \langle L^*_{\ell,\alpha,i}:i < 4\rangle be (but we can omit \ell) where:
(a) L^*_{\ell,\alpha,0} = L_0,
(b) L^*_{\ell,\alpha,1} = L_0 \cup \{s_\beta:\beta < \alpha\},
(c) L^*_{\ell,\alpha,2} = \{s \in L_{\mathbf m_\ell}:s \le_{\mathbf m_\ell} t for some t \in L_0\},
(d) L^*_{\ell,\alpha,3} = L_{\mathbf m_\ell},
\oplus_4
(a) (\bar{\mathbf m}_\ell,\bar L^*_{\ell,\alpha}) satisfies the assumption of 1.24,
(b) {\mathbb P}_{\mathbf m_\ell}(L^*_{\ell,\alpha,1}) \lessdot {\mathbb P}_{\mathbf m_\ell}(L^*_{\ell,\alpha,3}).
[Why? Note the \mathbf m_\ell,\langle L^*_{\ell,\alpha,i}:i < 4\rangle satisfies the assumptions of 1.24, hence \oplus_2 holds for \mathbf m_\ell,\bar L_{\ell,\alpha} for \alpha \le \alpha(*).]
Now by induction on \alpha \le \alpha(*) we prove that:
\boxplus_\alpha {\mathbb P}_{\mathbf m_1}(L^*_{\alpha,1}) = {\mathbb P}_{\mathbf m_2}(L^*_{\alpha,1}).
Case 1: \alpha = 0:
As L^*_{1,\alpha,1} = L_0 = L^*_{2,\alpha,1}, clause \boxdot(d) of the assumption gives \boxplus_\alpha as promised.
Case 2: \alpha a limit ordinal:
Easy by the definition of the iteration. That is, first, if {\rm dom}(p) \in [L_{\mathbf{m} _2}]^{\le \lambda } then we know p
\in {\mathbb P}_{\mathbf m_1}(L^*_{\alpha,1}) \Leftrightarrow \bigwedge\limits_{\beta < \alpha}
[p {\restriction} L^*_{\beta,1} \in {\mathbb P}_{\mathbf m_1}(L^*_{\beta,1})] \Leftrightarrow \bigwedge\limits_{\beta < \alpha}
[p {\restriction} L^*_{\beta,1} \in {\mathbb P}_{\mathbf m_2}(L^*_{\beta,1})] \Leftrightarrow p \in {\mathbb P}_{\mathbf m_2}(L^*_{\alpha,1}); second, for p,q \in {\mathbb P}_{\mathbf m_1}(L^*_{\alpha,1}) by the definition of the order and the induction hypothesis, {\mathbb P}_{\mathbf m_1}(L^*_{\alpha,1}) \models ``p \le q" iff \bigwedge\limits_{\beta < \alpha} [{\mathbb P}_{\mathbf m_1}(L^*_{\beta,1}) \models ``p {\restriction} L^*_{\beta,1} \le q
{\restriction} L^*_{\beta,1}"] iff \bigwedge\limits_{\beta < \alpha}
[{\mathbb P}_{\mathbf m_2}(L^*_{\beta,1}) \models ``p {\restriction} L^*_{\beta,1} \le q
{\restriction} L^*_{\beta,1}"] iff {\mathbb P}_{\mathbf m_2}(L^*_{\alpha,1}) \models ``p \le q".
So \boxplus_\alpha holds.
Case 3: \alpha = \beta +1:
Clearly,
(*)_1 p \in {\mathbb P}_{\mathbf m_1}(L^*_{\alpha,1}) \Leftrightarrow
p \in {\mathbb P}_{\mathbf m_2}(L^*_{\alpha,1}).
Next,
(*)_2 assume p,q \in {\mathbb P}_{\mathbf m_1}(L^*_{\alpha,1}) and we shall prove that {\mathbb P}_{\mathbf m_1}(L^*_{\alpha,1}) \models ``p \le q" implies {\mathbb P}_{\mathbf m_2}(L^*_{\alpha,1}) \models ``p \le q".
[Why? If s_\beta \notin {\rm dom}(p) this is obvious by the induction hypothesis. Hence we can assume s_\beta \in {\rm dom}(p), so as we are assuming {\mathbb P}_{\mathbf m_1}(L^*_{\alpha,1}) \models ``p \le q", clearly s_\beta \in {\rm dom}(q) hence s_\beta \in {\rm dom}(p) \cap {\rm dom}(q). First, similarly {\mathbb P}_{\mathbf m_1}(L^*_{\beta,1}) \models ``(p {\restriction} L^*_{\beta,1}) \le (q {\restriction} L^*_{\beta,1})" and (q {\restriction} L^*_{\beta,1}) {\Vdash_{{\mathbb P}_{{\mathbf m}_{1} (<s_{\beta})}}} ``p(s_\beta) \le_{{\mathbb Q}_{\bar\theta}} q(s_\beta)" by the definition of {\mathbb P}_{\mathbf m_1}(L^*_{\beta,1}). Second, as q {\restriction} L^*_{\beta,1} \in {\mathbb P}_{\mathbf m_1}(L^*_{\beta,1}) = {\mathbb P}_{\mathbf m_2}(L^*_{\beta,1}) and {\mathbb P}_{\mathbf m_1}(L^*_{\beta,1}) \lessdot
{\mathbb P}_{\mathbf m_1 } by \oplus_4 and {\mathbb P}_{\mathbf m_2}(L^*_{\beta,1})
\lessdot {\mathbb P}_{\mathbf m_2} by \oplus_4 and p(s_\beta), q(s_\beta) are {\mathbb P}_{\mathbf m_1}(L^*_{\beta,1})-names (as {\rm fsupp}(p(s_\beta),{\rm fsupp}(q(s_\beta))
\subseteq L^*_{\beta,1}) necessarily we have q {\restriction} L^*_{\beta,1} \Vdash_{{\mathbb P}_{\mathbf m_2}} ``p(s_\beta) \le_{{\mathbb Q}_{\bar\theta}}
q(s_\beta)". Third, as {\mathbb P}_{\mathbf m_1}(L^*_{\beta,1}) \models ``p {\restriction} L^*_{\beta,1} \le q {\restriction} L^*_{\beta,1}", by the induction hypothesis {\mathbb P}_{\mathbf m_2}
(L^*_{\beta,1}) \models ``p {\restriction} L^*_{\beta,1} \le q {\restriction} L^*_{\beta,1}. Fourth, by the last two sentence and the definition of the order in {\mathbb P}_{\mathbf m_2} we have {\mathbb P}_{\mathbf m_2} \models ``p \le
q" so the conclusion of (*)_2 holds also in this case.
Note that if s_\beta \in {\rm dom}(p) \backslash {\rm dom}(q) then p \nleq q, so we are done proving (*)_2.]
(*)_3 if p,q \in {\mathbb P}_{\mathbf m_1} (L^*_{\alpha,1}) and {\mathbb P}_{\mathbf m_2}(L^*_{\alpha,1}) \models ``p \le q" then {\mathbb P}_{\mathbf m_1}(L^*_{\alpha,1}) \models ``p \le q".
[Why? Similar to the proof of (*)_2.]
By (*)_1,(*)_2,(*)_3 clearly \boxplus_\alpha holds. So we carried the induction so \boxplus_\alpha holds for every \alpha \le \alpha(*) and for \alpha = \alpha(*) we get {\mathbb P}_{\mathbf m_1}(L_1) = {\mathbb P}_{\mathbf m_2}(L_2). Together with \oplus_2(b) in the beginning of the proof we are done.