theorem Th21: :: FOMODEL2:21

for S being Language
for U being non empty set
for t being termal string of S
for I being b₁,b₂ -interpreter-like Function holds (I -TermEval) . t = (I . ((S -firstChar) . t)) . ((I -TermEval) * (SubTerms t))