The Hecke tower is free over the previous level

Coset representatives. For $0\le i\le n$ the permutation $w^{(i)}=s_n{s}_{n-1}\cdots s_{n-i+1}$ has length $i$ and satisfies $w^{(i)}(n+1)=n$ for $i\ge 1$, while $w^{(0)}=\mathrm{i}\mathrm{d}$ fixes $n+1$; equivalently $w^{(i)-1}(n+1)=n-i+1$. Since two elements of $S_{n+1}$ lie in the same left coset of $S_n$ exactly when their inverses send $n+1$ to the same point, the $w^{(i)}$ form a complete set of left coset representatives: $S_{n+1}={⨆}_{i=0}^n{S}_n{w}^{(i)}$.

Length additivity. Every $v\in S_n$ satisfies $\mathrm{\ell }(v{w}^{(i)})=\mathrm{\ell }(v)+i$. Indeed $w^{(i)}=w^{(i-1)}{s}_{n-i+1}$ and $w^{(i-1)}(n-i+1)=n-i+1<n+1=w^{(i-1)}(n-i+2)$. For $v\in S_n$, $v$ fixes $n+1$ and maps $\{1,\dots ,n\}$ to itself, so $(v{w}^{(i-1)})(n-i+1)=v(n-i+1)\le n<n+1=v(n+1)=(v{w}^{(i-1)})(n-i+2)$. The ascent criterion in [F3] therefore gives $\mathrm{\ell }(v{w}^{(i)})=\mathrm{\ell }(v{w}^{(i-1)})+1$. Induction on $i$ yields $\mathrm{\ell }(v{w}^{(i)})=\mathrm{\ell }(v)+i$, and in particular $\mathrm{\ell }(w^{(i)})=i$. Length-additive products of reduced words are reduced, so [F2] gives $T_v{T}_{w^{(i)}}=T_{v{w}^{(i)}}$. Taking inverses also gives $\mathrm{\ell }((w^{(i)}{)}^{-1}v)=i+\mathrm{\ell }(v)$ and $T_{(w^{(i)}{)}^{-1}}{T}_v=T_{(w^{(i)}{)}^{-1}v}$ for every $v\in S_n$.

The module bases. By step 1.1 and step 2.1, the elements $v{w}^{(i)}$, $v\in S_n$, $0\le i\le n$, are exactly the elements of $S_{n+1}$, each occurring once. Hence $\{T_{v{w}^{(i)}}\}$ is the standard $\mathrm{\Lambda }$-basis of $H(n+1)$ by [F1], and $T_{v{w}^{(i)}}=T_v{T}_{w^{(i)}}$. Regrouping by $i$ proves part (1). For the right module, invert the left-coset decomposition $S_{n+1}={⨆}_i{S}_n{w}^{(i)}$ to obtain $S_{n+1}={⨆}_i(w^{(i)}{)}^{-1}{S}_n$. The length-additive formulas of step 2.1 show that the resulting standard-basis elements are $T_{(w^{(i)}{)}^{-1}}{T}_v$ for $v\in S_n$, each exactly once; regrouping by $i$ proves the stated right-module basis.

The sub-bimodule and the tensor decomposition. For $i\ge 1$, the reduced word $w^{(i)}=s_n{s}_{n-1}\cdots s_{n-i+1}$ begins with $s_n$, so $T_{w^{(i)}}\in T_{n}H(n)$ and $H(n)T_{w^{(i)}}\subseteq H(n)T_{n}H(n)$. This proves ${⨁}_{i=1}^{n}H(n)T_{w^{(i)}}\subseteq H(n)T_{n}H(n)$. Conversely, for every $v\in S_n$, $\mathrm{\ell }(s_{n}v)=\mathrm{\ell }(v)+1$: indeed $\mathrm{\ell }(s_{n}v)=\mathrm{\ell }(v^{-1}{s}_n)$ by invariance of length under inversion, and $v^{-1}\in S_n$ fixes $n+1$, so right multiplication by $s_n$ is an ascent. Thus $T_n{T}_v=T_{s_{n}v}$ by concatenating reduced words. The permutation $s_{n}v$ does not fix $n+1$, since $(s_{n}v)(n+1)=n$; hence in the left-coset decomposition of step 1.1 it belongs to a coset $S_n{w}^{(i)}$ with $i\ge 1$. By step 2.1, $T_{s_{n}v}=T_a{T}_{w^{(i)}}$ for some $a\in S_n$. Since the $T_v$ form a $\mathrm{\Lambda }$-basis of $H(n)$ by [F1], this shows $T_{n}H(n)\subseteq {⨁}_{i=1}^{n}H(n)T_{w^{(i)}}$, and left multiplication by $H(n)$ gives the reverse inclusion for the generated sub-bimodule. Therefore $H(n)T_{n}H(n)={⨁}_{i=1}^{n}H(n)T_{w^{(i)}}$. Thus step 3.1 gives $H(n+1)=H(n)\oplus H(n)T_{n}H(n)$ as $H(n)$-bimodules.

The tensor isomorphism over $\mathrm{\Lambda }$. For $0\le j\le n-1$ put $b_j=T_{n-1}{T}_{n-2}\cdots T_{n-j}$, with $b_0=1$. Applying part (1), already proved in step 3.1, at level $n-1$ gives $H(n)={⨁}_{j}H(n-1)b_j$ as a left module; for $n=1$ this is simply $H(1)=H(0)=\mathrm{\Lambda }$. Consequently every tensor has a unique form ${\sum }_j{a}_j\otimes b_j$, $a_j\in H(n)$. Explicitly, if $y={\sum }_j{h}_j{b}_j$, balancing sends $x\otimes y$ to the coefficient tuple $(x{h}_j{)}_j$; this is additive and balanced, and is inverse to $(a_j{)}_j\mapsto {\sum }_j{a}_j\otimes b_j$. By [F5], $\mu (x\otimes y)=x{T}_{n}y$ is well defined and an $H(n)$-bimodule map. It sends $a_j\otimes b_j$ to $a_j{T}_{w^{(j+1)}}$. These form the unique left-module coordinates of $H(n)T_{n}H(n)$ from step 4.1, so $\mu$ is bijective. This proves part (3).