Since C as in Lemma 2.2 is universal, \mathbb H_E forces that \prod_{\operatorname{Fin}} (A_n, \triangleleft_n) has a \kappa-chain for some sequence (A_n,\triangleleft_n) (not necessarily in the ground model) if and only if \mathbb H_E forces that (C^{\mathbb N},\triangleleft^*):=\prod_{\operatorname{Fin}} (C,\triangleleft) has a \kappa chain. It will therefore suffice to prove the theorem with the additional assumption that (A_n,\triangleleft_n)=(C,\triangleleft) for all n.
Assume that \dot f_\xi, for \xi<\kappa, is a name for a \kappa-chain in (C^{\mathbb N},\triangleleft^*). (We emphasize that this means that for all \xi<\eta, \mathbb H_E forces both \dot f_\xi\triangleleft^* \dot f_\eta and \dot f_\eta\ntriangleleft^* \dot f_\xi.) The ccc-ness of \mathbb H_E implies that for every limit ordinal \xi there exists a countable E(\xi)\subseteq E such that \dot f_\xi, \dot f_{\xi+1}, and \dot f_{\xi+2} are \mathbb H_{E(\xi)}-names. Since \kappa is regular and \lambda^{\aleph_0}<\kappa for all \lambda<\kappa, the \Delta-system lemma for countable sets implies that any family of \kappa countable sets includes a \Delta-system of cardinality \kappa. By passing to a subfamily, we may assume that the sets E(\xi) form a \Delta-system with a countable root A.
For every limit ordinal \xi fix q_\xi\in \mathbb H_E and n\in {\mathbb N} such that
q_\xi\Vdash_{\mathbb H_E} \dot f_\xi\triangleleft^n \dot f_{\xi+1}
\triangleleft^n \dot f_{\xi+2}.
By the pigeonhole principle and passing to a subfamily if necessary, we may assume that n as in (?) is the same for all \xi. Lemma 4.7 implies that \mathbb H_{E(\xi)} is a regular subordering of \mathbb H_E. We may therefore assume that q_\xi\in \mathbb H_{E(\xi)} and we have
q_\xi\Vdash_{ \mathbb H_{E(\xi)}} \dot f_\xi\triangleleft^n \dot f_{\xi+1}
\triangleleft^n \dot f_{\xi+2}.
Writing q_\xi=(D_\xi,n_\xi, f_\xi), let F(\xi):=D_{\xi}\setminus A. Note that each F(\xi) is finite.
Fix \xi<\kappa for a moment and fix a generic filter G\subseteq \mathbb H_{A\cup F(\xi)} such that q_\xi\in G. Recall that the domain of C is {\mathbb N}, and is therefore equipped with a well-ordering (as a matter of fact, the first well-ordering known to man). For j\in{\mathbb N} we can let h_\xi(j) be the least element of C (in this well-ordering) such that
r\Vdash \dot f_{\xi+1}(j)=\check c
for some r in the quotient \mathbb H_E(A\cup F(\xi),\Upsilon_G)/G (see Lemma 4.10).
This defines h_\xi\in C^{\mathbb N} in V[G]. Use the Maximality Principle ([Ku:Set, Theorem IV.7.1]) to choose an \mathbb H_{A\cup F(\xi)}-name \dot h_\xi for this function.
Claim. The condition q_\xi forces that \dot f_\xi\triangleleft^n \dot h_\xi\triangleleft^n f_{\xi+2}.
Proof. If there are r\leq q_\xi in \mathbb H_E and j\geq n such that r\Vdash \dot f_\xi(j)\ntriangleleft \dot h_\xi(j), fix a generic filter G in \mathbb H_E containing r. Then in V[G] we have \dot f_\xi\ntriangleleft^n \dot f_{\xi+1}, although q_\xi\in G; contradiction. An analogous argument gives that there is no j\geq n such that some r\leq_E q_\xi forces that \dot h_\xi(j)\ntriangleleft \dot f_{\xi+2}(j).
The pairs (q_\xi,\dot h_\xi) are indexed by limit ordinals below \kappa. We re-enumerate them preserving the order and obtain conditions q_\xi and names \dot h_\xi for \xi<\kappa. Since \mathbb H_E has the ccc, some condition q\in \mathbb H_E forces that \kappa of the q_\xi’s belong to the generic filter. Therefore q forces that the family of all h_\xi such that q_\xi belongs to the generic filter is a \kappa-chain in (C^{\mathbb N}, \triangleleft^*).
By Proposition 3.9, there exists a cofinal X\subseteq \kappa such that for any two distinct elements \xi<\eta of X there is s\Subset \kappa such that \{\xi,\eta\}=\{\min(s),\max(s)\} and there is no s-walk with endpoints in F(\xi) and F(\eta).
Fix \xi\in X, let \xi':=\min(X\setminus (\xi+1)), and fix s\Subset \kappa such that \{\xi,\xi'\}=\{\min(s),\max(s)\} and there is no s-walk with endpoints in F(\xi) and F(\xi'). We will analyze the relation between the names \dot h_{\xi} and \dot h_{\xi'}.
Let \xi(j), for j<n,(This n is unrelated to the n appearing in ?. No danger of confusion here.) be an increasing enumeration of s, so that in particular \xi(0)=\xi and \xi(n-1)=\xi'. Consider the depletion \ll_s of \leq_E given by A and F(\eta), for \eta\in s. By Lemma 3.4, \ll_s is a partial ordering on
A':=A\cup\bigcup_{j<n} F(\xi(j)).
For i<j<n let
A(i,j):=A\cup F(\xi(i))\cup F(\xi(j)),
ordered by \ll_s. Note that if |i-j|>1 then A(i,j) is ordered by a restriction of the depletion associated with s which can differ from the natural depletion \ll_{(\xi(i), \xi(j))} (Remark 3.7). However, for i<n-1, Lemma 3.8 implies that the restriction of \ll_s to A(i,i+1) agrees with the depletion \ll_{\{\xi(i),\xi(i+1)\}}, which by Lemma 3.2 agrees with the ordering induced from E. By Lemma 4.7, we have \mathbb H_{A(i,i+1)}\lessdot \mathbb H_E.
Since A' is ordered by \ll_s, which possibly disagrees with the ordering of A' inherited from E, the posets \mathbb H_{A'} and \mathbb H_E are possibly unrelated. On the other hand, each A(i,j) is a subordering of A' and therefore Lemma 4.7 implies \mathbb H_{A(i,j)}\lessdot \mathbb H_{A'}.
Since \dot h_{\xi(i)} and \dot h_{\xi(j)} are \mathbb H_{A(i,j)}-names and \mathbb H_E forces \dot h_{\xi(i)}\triangleleft^* \dot h_{\xi(i+1)} for all i<n-1, we have that \mathbb H_{A'} forces \dot h_{\xi(i)}\triangleleft^* \dot h_{\xi(i+1)} for all i<n-1. By transitivity, \mathbb H_{A'} forces \dot h_{\xi(0)}\triangleleft^* \dot h_{\xi(n-1)}. Since \dot h_{\xi(0)} and \dot h_{\xi(n-1)} are \mathbb H_{A(0,n-1)}-names and \mathbb H_{A(0,n-1)}\lessdot \mathbb H_{A'}, we have that \mathbb H_{A(0,n-1)} forces \dot h_{\xi(0)}\triangleleft^* \dot h_{\xi(n-1)}.
Since there is no s-walk whose endpoints are some x\in F(\xi(0)) and some y\in F(\xi(n-1)), we have that x\ll_s y implies there is a\in A such that x\leq a\leq y, and that y\ll_s x imples there is a\in A such that y\leq a\leq x. This means that the assumptions of Lemma 4.12 with E, A, B, and D replaced with A\cup F(\xi(0))\cup F(\xi(n-1)), A\cup F(\xi(0)), A\cup F(\xi(n-1)), and A, respectively, (sorry!) are satisfied. Therefore if G\subseteq \mathbb H_A is a generic filter then the quotient \mathbb H_{A\cup A(0,n-1)}/G is forcing-equivalent to the product
\mathbb H_{A\cup F(\xi(0)}(A,\Upsilon_{G})
\times \mathbb H_{A\cup F(\xi(n-1))}(A,\Upsilon_{G}).
Most importantly, the names \dot h_{\xi(0)} and \dot h_{\xi(n-1)} are added by the two factors of this product. By Lemma 4.11, there exist a condition p_\xi\in \mathbb H_A and an \mathbb H_A-name \dot g_\xi (recall that \xi=\xi(0)) such that
p_\xi\Vdash \dot h_{\xi(0)}\leq^* \dot g_\xi\leq^* \dot h_{\xi(n-1)}.
Since \mathbb H_A is countable, there is q\in \mathbb H_A such that Y=\{\xi\in X\vert p_\xi=q\} is a cofinal subset of X (and of \kappa). Therefore q forces that \mathbb H_A adds a strictly increasing \kappa-chain \dot g_\xi, for \xi<\kappa, to ({\mathbb N}^{{\mathbb N}},\leq^*). Since A is countable, \mathbb H_A cannot add more than \mathfrak c reals; contradiction.