Item 2. If $p \in Pos(s)$ and $q \in Pos(t)$:
2.1 $(s[t]{p})|{pq} = t|_{q}$.
We prove by induction on the length of $p$:
Case $p = \epsilon$:
$(s[t]{\epsilon})|{\epsilon q} = t|{\epsilon q} = t|{q}$.
Case $p = ip'$:
$(s[t]{ip'})|{ip'q} = f(s_1, \ldots, s_i[t]{p'}, \ldots, s_n)|{ip'q} = (s_{i}[t]{p'})|{p'q}$. By induction hypothesis, $(s_{i}[t]{p'})|{p'q} = t|_{q}$.
2.2 $(s[t]{p})[r]{pq} = s[t[r]{q}]{p}$.
We prove by induction on the length of $p$:
Case $p = \epsilon$:
Notice that $(s[t]{\epsilon})[r]{\epsilon q} = t[r]{q}$ and also that: $s[t[r]{q}]{\epsilon} = t[r]{q}$.
Case $p = ip'$:
$(s[t]{ip'})[r]{ip'q} = f(s_1, \ldots, s_{i}[t]{p'}, \ldots, s_n)[r]{ip'q} = f(s_1, \ldots, (s_{i}[t]{p'})[r]{p'q}, \ldots, s_n)$. 532
By induction hypothesis, $$(s_{i}[t]{p'})[r]{p'q} = s_i[t[r]{q}]{p'}$$ and hence $f(s_1, \ldots, (s_{i}[t]{p'})[r]{p'q}, \ldots, s_n) = f(s_1, \ldots, s_i[t[r]{q}]{p'}, \ldots, s_n) = s[t[r]{q}]{ip'}$.
Item 3. If $pq \in Pos(s)$, then :
3.1 $(s[t]{pq})|{p} = (s|{p})[t]{q}$.
We prove by induction on the length of $p$:
Case $p = \epsilon$:
notice that $(s[t]{\epsilon q})|{\epsilon} = s[t]{q}$ and also that $(s|{\epsilon})[t]{q} = s[t]{q}$.
Case $p = ip'$:
$(s[t]{ip'q})|{ip'} = f(s_1, \ldots, s_{i}[t]{p'q}, \ldots, s_n)|{ip'} = (s_{i}[t]{p'q})|{p'}$. By induction hypothesis:
$$(s_{i}[t]{p'q})|{p'} = (s_{i}|{p'})[t]{q}$$
But $(s|{ip'})[t]{q} = (s_{i}|{p'})[t]{q}$ and thus the result holds.
3.2 $(s[t]{pq})[r]{p} = s[r]_{p}$.
We prove by induction on the length of $p$:
Case $p = \epsilon$:
$(s[t]{\epsilon q})[r]{\epsilon} = r = s[r]_{\epsilon}$. 532