Es seien ${\displaystyle {}x,y}$ Variablen, ${\displaystyle {}s,t}$ Terme und ${\displaystyle {}\alpha }$ ein Ausdruck in einer prädikatenlogischen Sprache. Es seien ${\displaystyle {}u,v}$ neue Variablen, die weder in ${\displaystyle {}s}$ noch in ${\displaystyle {}t}$ noch in ${\displaystyle {}\alpha }$ vorkommen. Zeige, dass

${\displaystyle \alpha {\frac {s,t}{x,y}}\leftrightarrow \alpha {\frac {s{\frac {v}{y}}}{x}}{\frac {t{\frac {u}{x}}}{y}}{\frac {x}{u}}{\frac {y}{v}}}$

allgemeingültig ist, wobei der Ausdruck rechts als die Hintereinanderausführung von vier Einzelsubstitutionen (von links nach rechts)