for m, n being Nat
for S being Language
for U being non empty set
for u1, u2 being Element of U
for I being b₃,b₄ -interpreter-like Function
for t being b₁ -termal string of S holds (((I,u1) -TermEval) . (m + 1)) . t = (((I,u2) -TermEval) . ((m + 1) + n)) . t by Lm6;