let m be 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 b1,b2 -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)) . {} ) )
let S be Language; for U being non empty set
for u being Element of U
for t being termal string of S
for I being S,b1 -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)) . {} ) )
let U be non empty set ; for u being Element of U
for t being termal string of S
for I being S,U -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)) . {} ) )
let u be Element of U; for t being termal string of S
for I being S,U -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)) . {} ) )
let t be termal string of S; for I being S,U -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)) . {} ) )
let I be S,U -interpreter-like Function; ( (((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)) . {} ) )
reconsider mm = m as Element of NAT by ORDINAL1:def 12;
( (((I,u) -TermEval) . (mm + 1)) . t = (I . ((S -firstChar) . t)) . ((((I,u) -TermEval) . mm) * (SubTerms t)) & ( t is 0 -termal implies (((I,u) -TermEval) . (mm + 1)) . t = (I . ((S -firstChar) . t)) . {} ) )
by Lm5;
hence
( (((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)) . {} ) )
; verum