I'm unsure of the exact form of the I.H. in this case (the $\exists_x B \in Wff(M)$ rule).
I was thinking it could be $(B[x \leftarrow t])^\mathcal{J} = (B[x \leftarrow \bar i])^\mathcal{J}$, but it is possible that $w$ occurs free in $B$, so interpretation may not be defined ($B$ is not closed).
But in the proof he says $((B[w \leftarrow \bar j])[x \leftarrow \bar i])^\mathcal{J}$ comes from I.H., so does this mean that I.H. is:
For any $m \in M$, $(B[w \leftarrow \bar m][x \leftarrow t])^\mathcal{J} = (B[w \leftarrow \bar m][x \leftarrow \bar i])^\mathcal{J}$ ?
Is this correct? Are we allowed to say something like this?
First line of the proof : the formula $\mathscr A$ is written in full.
Second step, the substitution $[x \leftarrow t]$ acts only on the formula $\mathscr B$ in the scope of the quantifier.
Third line : the semantic clause for the existential quantifier is applied (Def.1.5.6, page 55). Here we have an object $j \in M$ ad we use the corresponding term : $\overline j$.
Fourth line : the two substitutions commute (already proved).
Fifth line : the simultaneous substitution is transformed into two successive substitutions.
According to the statement of the Lemma, $\mathscr A$ has only $x$ free.
Thus, $\mathscr A [x \leftarrow t] := ((\exists w) \mathscr B)[x \leftarrow t])$ has no free variables.
When we remove the leading existential quantifier, formula $\mathscr B [x \leftarrow t]$ has only $w$ free, and thus $(\mathscr B [x \leftarrow t][w \leftarrow \overline j])$ has no free variables.
This in turn means that $\mathscr B [w \leftarrow \overline j]$ has only one free variable : $x$.
But formula $\mathscr B [w \leftarrow \overline j]$ has a "lower complexity" than $\mathscr A$, and thus we apply the Induction Hypotheses : sixth line.
This means that, according to the I.H., the formula $((\mathscr B [w \leftarrow \overline j])[x \leftarrow t])$ - that is, the formula $\mathscr B [w \leftarrow \overline j]$ with $x$ free where we have substituted the term $t$ in place of $x$ - has the same truth value of formula $((\mathscr B [w \leftarrow \overline j])[x \leftarrow \overline i])$, where $\overline i$ is the term associated to element $i \in M$ such that :