theorem Th3: :: FOMODEL2:3

for m being Nat
for S being Language
for U being non empty set
for u being Element of U
for t being termal string of S
for I being b₂,b₃ -interpreter-like Function holds
( (((I,u) -TermEval) . (m + 1)) . t = (I . ((S -firstChar) . t)) . ((((I,u) -TermEval) . m) * (SubTerms t)) & ( t is 0 -termal implies (((I,u) -TermEval) . (m + 1)) . t = (I . ((S -firstChar) . t)) . {} ) )