Es sei ein Symbolalphabet S {\displaystyle {}S} einer Sprache erster Stufe gegeben. Es seien x 1 , … , x k , y 1 , … , y ℓ {\displaystyle {}x_{1},\ldots ,x_{k},y_{1},\ldots ,y_{\ell }} paarweise verschiedene Variablen und t 1 , … , t k , s 1 , … , s ℓ {\displaystyle {}t_{1},\ldots ,t_{k},s_{1},\ldots ,s_{\ell }} fixierte S {\displaystyle {}S} -Terme. Zeige, dass für Terme τ {\displaystyle {}\tau } , in denen y 1 , … , y ℓ {\displaystyle {}y_{1},\ldots ,y_{\ell }} nicht vorkommen, die Gleichheit
gilt.