for S being Language
for U being non empty set
for p being FinSequence
for u being Element of U
for l2 being literal Element of S
for I being b₁,b₂ -interpreter-like Function st not l2 in rng p holds
(((l2,u) ReassignIn I) -TermEval) . p = (I -TermEval) . p