Lambda calculus :Will there be any x left after first substitution? I found the following set of lemma in my lambda calculus textbook :


  Lemma 1.16 Let $x, y, v$ be distinct (the usual notation convention), and let no variable bound in $M$ be free in $vPQ$. Then
  
  (a) $[P/v][v/x]M \equiv [P/x]M$ if $v \notin \mathrm{FV}(M)$;
  
  (b) $[x/v][v/x]M \equiv M$ if $v \notin \mathrm{FV}(M)$;
  
  (c) $[P/x][Q/y]M \equiv [([P/x]Q)/y][P/x]M$ if $y \notin \mathrm{FV}(P)$;
  
  (d) $[P/x][Q/y]M \equiv [Q/y][P/x]M$ if $y \notin \mathrm{FV}(P), x \notin \mathrm{FV}(Q)$;
  
  (e) $[P/x][Q/x]M \equiv [([P/x]Q)/x]M$.


I am stuck at (e) .I wonder if there is any order to be followed while evaluating this kind of expressions or there isn't any .What I think is that in $[P/x][Q/x]M $ we would replace all the $ x $ in $ M $ by $ Q $ and as such we wouldn't be having any more $ x $ to be replaced by $ P $ . Then there is no point in the the exterior substitution expression ,i.e. $ [P/x] $ . How to explain this ?
After $[Q/x]M$ we no longer find free occurrences of $x$ ... unless $x$ is free in $Q$! The simpler example is $Q=x$, where $[x/x]M=M$ can have free occurrences of $x$.

In such case, the free $x$s due to $Q$ can be replaced by $[P/x]$ in your example.

E.g. $[z/x][(\lambda y.\ x)/x](x(yx)) = ((\lambda y.\ z)(y(\lambda y.\ z)))$.

According to (e) we have indeed

$$
\begin{array}{l}
[z/x][(\lambda y.\ x)/x](x(yx)) \\
= [[z/x](\lambda y.\ x)/x](x(yx))\\
= [(\lambda y.\ z)/x](x(yx))\\
= ((\lambda y.\ z)(y(\lambda y.\ z)))
\end{array}
$$

Finally, note that when $x$ is not free in $Q$, we have
$[[P/x]Q/x]M = [Q/x]M$ as an immediate consequence of $[P/x]Q=Q$.