:: deftheorem Def9 defines -TermEval FOMODEL2:def 10 :
for S being Language
for U being non empty set
for I being b₁,b₂ -interpreter-like Function
for b₄ being Function of (AllTermsOf S),U holds
( b₄ = I -TermEval iff for t being Element of AllTermsOf S holds b₄ . t = I -TermEval t );