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 b1,b2 -interpreter-like Function holds
( (((I,u) -TermEval) . (m + 1)) . t = (I . (() . t)) . ((((I,u) -TermEval) . m) * ()) & ( t is 0 -termal implies (((I,u) -TermEval) . (m + 1)) . t = (I . (() . 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,b1 -interpreter-like Function holds
( (((I,u) -TermEval) . (m + 1)) . t = (I . (() . t)) . ((((I,u) -TermEval) . m) * ()) & ( t is 0 -termal implies (((I,u) -TermEval) . (m + 1)) . t = (I . (() . 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 . (() . t)) . ((((I,u) -TermEval) . m) * ()) & ( t is 0 -termal implies (((I,u) -TermEval) . (m + 1)) . t = (I . (() . 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 . (() . t)) . ((((I,u) -TermEval) . m) * ()) & ( t is 0 -termal implies (((I,u) -TermEval) . (m + 1)) . t = (I . (() . 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 . (() . t)) . ((((I,u) -TermEval) . m) * ()) & ( t is 0 -termal implies (((I,u) -TermEval) . (m + 1)) . t = (I . (() . t)) . {} ) )

let I be S,U -interpreter-like Function; :: thesis: ( (((I,u) -TermEval) . (m + 1)) . t = (I . (() . t)) . ((((I,u) -TermEval) . m) * ()) & ( t is 0 -termal implies (((I,u) -TermEval) . (m + 1)) . t = (I . (() . t)) . {} ) )
reconsider mm = m as Element of NAT by ORDINAL1:def 12;
( (((I,u) -TermEval) . (mm + 1)) . t = (I . (() . t)) . ((((I,u) -TermEval) . mm) * ()) & ( t is 0 -termal implies (((I,u) -TermEval) . (mm + 1)) . t = (I . (() . t)) . {} ) ) by Lm5;
hence ( (((I,u) -TermEval) . (m + 1)) . t = (I . (() . t)) . ((((I,u) -TermEval) . m) * ()) & ( t is 0 -termal implies (((I,u) -TermEval) . (m + 1)) . t = (I . (() . t)) . {} ) ) ; :: thesis: verum