1: \begin{proof} Induction on the structure of $M$.\\[5pt]

2: Case 1. If $M=\lambda\x N$ then\\

3: $F(db_{\z}(\lambda\x N))=F\lambda\z\{\z\x\}db_{\z}(N)=\lambda\z F_{\z}\{\z\x\}db_{\z}(N)=\lambda\z\{\z\x\} F_{\x}\,db_{\z}(N)$\\

4: the last equality by Lemma~\ref{Commute}\\

5: $db_{\z}(F\lambda\x N)=db_{\z}(\lambda\x F_{\x}N)=\lambda\z\{\z\x\}db_{\z}(F_{\x}N)$\\

6: but $F_{\x}\,db_{\z}(N)=db_{\z}(F_{\x}N)$ by induction hypothesis.\\[5pt]

7: Case 2. If $M$ is a variable $\y$ then\\

8:  $F(db_{\z}\y)=F\y$\\

9:  $db_{\z}(F\y)=F\y$ because $F\y$ always is a variable or $\underbrace{\up\ldots\up}_{n}$ var.\\

10:  More rigorously, use induction on the structure of $F$ (see Tab.~\ref{Terms}).\\

11:  Suppose $F$ is $\{\x_1\x_2\}$ and prove\\

12:  $db_{\z}(\{\x_1\x_2\}\y)=\{\x_1\x_2\}\y$\\

13:  If $\y=\x_2$ then\\

14:  $db_{\z}(\{\x_1\x_2\}\x_2)=db_{\z}(\x_1)=\x_1=\{\x_1\x_2\}\x_2$\\

15:  If $\y\neq\x_2$ then\\

16:  $db_{\z}(\{\x_1\x_2\}\y)=db_{\z}(\up\y)=\,\up db_{\z}(\y)=\,\up\y=\{\x_1\x_2\}\y$\\

17:  Now prove the induction step\\[5pt]

18:  \ruleone{db_{\z}(F\y)=F\y}{db_{\z}(F_{\x}\y)= F_{\x}\y}\\[5pt]

19:  If $\y=\x$ then \\

20:  $db_{\z}(F_{\x}\,\x)=db_{\z}(\x)=\x= F_{\x}\,\x$\\

21:  If $\y\neq\x$ then\\

22:  $db_{\z}(F_{\x}\,\y)=db_{\z}(\up F\y)=\,\up db_{\z}(F\y)$\\

23:  $F_{\x}\,\y=\,\up F\y$\\[5pt]

24:  Case 3. Suppose $M=\,\up N$. \\

25:  If $F$ is $\{\x_2,\x_1\}$ then \\

26:  $\{\x_1,\x_2\}\,db_{\z}(\up N)=\{\x_1,\x_2\}\!\up db_{\z}(N)=\,\up db_{\z}(N)$\\

27:  $db_{\z}(\{\x_1,\x_2\}\!\up N)=db_{\z}(\up N)=\,\up db_{\z}(N)$\\

28:  If function has the form $F_{\x}$ then (induction on the structure of $M$)\\[5pt]

29:  \ruleone{db_{\z}(FN)=FN}{db_{\z}(F_{\x}\!\up N)= F_{\x}\!\up N}\\[5pt]

30:  because\\

31:  $db_{\z}(F_{\x}\!\up N)=db_{\z}(\up FN)=\,\up db_{\z}(FN)$\\

32:  $F_{\x}\!\up N=\,\up FN$\\[5pt]

33:  Case 4. $M=N_1N_2$\\

34:  Straighforward.

35: 

36: \end{proof}

37: