theorem :: FOMODEL3:4

for X being set
for S being Language holds ((S,X) -freeInterpreter) -TermEval = id (AllTermsOf S) by Lm29;