for X being set
for U being non empty set
for n being Nat
for S being Language
for l being literal Element of S
for I being b₄,b₂ -interpreter-like Function
for tt0 being Element of AllTermsOf S holds ((I -TermEval) * (((((l,tt0) ReassignIn ((S,X) -freeInterpreter)),tt0) -TermEval) . n)) | ((S -termsOfMaxDepth) . n) = (((((l,((I -TermEval) . tt0)) ReassignIn I),((I -TermEval) . tt0)) -TermEval) . n) | ((S -termsOfMaxDepth) . n)