The substitution lemma in lambda-calculus is proved by the following way, but I just did not understand the application of induction hypothesis in it.
The lemma as shown below, where $x$ and $y$ are distinct and $x$ is not among the free variables of $L$:
M[x:=N][y:=L] equals M[y:=L][x:=N[y:=L]]
to prove that in the case where $M= \lambda z.M_1$, by the variable convention, $z$ is distinct from $x$ and $y$, and $z$ is not among the free variables of $N$ and $L$. and The proof goes like this
(1) = (λz.M1)[ x:=N ] [ y:=L ]
(2) = λz.M1[ x:=N ] [ y:=L ] by susbtitution definition
(3) = λz.M1[ y:=L ] [ x:=N [ y:=L ] ] by induction hypothesis
(4) = (λz.M1)[ y:=L ] [ x:=N [ y:=L ] ] by susbtitution definition
so, it is proved.
I think 3th line is obtained by substitution definitions $(M_1 M_2)[x:=N] = (M_1[x:=N])(M_2[x:=N])$, right? Just did not see last line, how it is obtained? how induction hypothesis is applied? substitution lemma given here Can someone explain this point to me? Thanks in advance!
The proof of the substitution lemma for the case $\lambda z.M_1$ has nothing to do with the definition of substitution for the application.
By definition of substitution, $(\lambda z.M_1)[x:=N][y:=L] = \lambda z.(M_1[x:=N][y:=L])$ since the hypotheses about $x$ ensure that the substitutions can be moved inside the $\lambda$.
Since $M_1$ is a smaller term than $\lambda z.M_1$, the induction hypothesis can be applied to $M_1$. This means that you can use the statement that you want to prove for the term $M_1$ (see Wikipedia for more details about structural induction). Therefore, $M_1[x:=N][y:=L] = M_1[y:=L][x:=N[y:=L]]$ and hence $\lambda z.(M_1[x:=N][y:=L]) = \lambda z.(M_1[y:=L][x:=N[y:=L]])$.
By definition of substitution again, $\lambda z.(M_1[y:=L][x:=N [y:=L]]) = (\lambda z.M_1)[ y:=L ] [ x:=N [ y:=L ]] $ since the hypotheses about $x$ ensure that the substitutions can be moved outside the $\lambda$.