Proof: Fix $\phi\in T$, we will show $B\models\phi$. Let $\{s_i:i<n\}$ enumerate the symbols of $L\bez L_T$ occurring $\phi$, and for $i\le n$, let $A_i$ denote $A$ with the interpretation of $s_j$ changed to $s_j^B$ for each $j<i$. Applying $n$ times the definition of $L_T$, we see that $A_i\models T$ for each $i\le n$, thus $A_n\models\phi$. But $A_n$ and $B$ agree on all symbols that occur in $\phi$, hence $B\models\phi$. QED
Consequently, if $A\res L_T\models T\res L_T$, then $A\res L_T\models\{\phi':T\models\phi\}$, i.e., $(A\res L_T)_c\models T$ for any $c\in A$, and therefore $A\models T$ by Lemma 1. Thus, every model of $T\res L_T$ is a model of $T$. QEDQED
NB: In the first-order case, Lemma 2 can be proved in a somewhat more transparent way using the Craig interpolation lemma, but this is not available for second-order logic.
and observe that it makes (1) hold. QEDQED
Since $\ET_{i\le n}\psi_i$ is equivalent to $\ET_{i\le n}\phi_n$, $S\equiv T$. Moreover, since $\psi_n\in S$ is not valid, there is $A_n\models\neg\psi_n$. This means $A_n\models\phi_i$ for $i<n$ and $A_n\models\neg\phi_n$, which implies $A_n\models\{\psi_i:i\ne n\}$. Thus, $S$ is independent. QEDQED
