let m be Nat; :: thesis: 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)) . {} ) )
let S be Language; :: thesis: for U being non empty set
for u being Element of U
for t being termal string of S
for I being S,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)) . {} ) )
let U be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( (((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)) . {} ) ) ; :: thesis: verum