for U being non empty set
for S being Language
for E being Equivalence_Relation of U
for I being b₂,b₁ -interpreter-like b₃ -respecting Function holds (I quotient E) -TermEval = (E -class) * (I -TermEval) by Lm25;