let S be Language; :: thesis: for U being non empty set
for u being Element of U
for I being S,b1 -interpreter-like Function
for t being termal string of S
for mm being Element of NAT holds
( (((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)) . {} ) )

let U be non empty set ; :: thesis: for u being Element of U
for I being S,U -interpreter-like Function
for t being termal string of S
for mm being Element of NAT holds
( (((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)) . {} ) )

let u be Element of U; :: thesis: for I being S,U -interpreter-like Function
for t being termal string of S
for mm being Element of NAT holds
( (((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)) . {} ) )

let I be S,U -interpreter-like Function; :: thesis: for t being termal string of S
for mm being Element of NAT holds
( (((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)) . {} ) )

let t be termal string of S; :: thesis: for mm being Element of NAT holds
( (((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)) . {} ) )

let mm be Element of NAT ; :: thesis: ( (((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)) . {} ) )
set TE = (I,u) -TermEval ;
set F = S -firstChar ;
set ST = S -subTerms ;
set A = AllTermsOf S;
A1: ( t in AllTermsOf S & AllTermsOf S c= dom (I * ()) ) by ;
reconsider tt = t as Element of AllTermsOf S by FOMODEL1:def 32;
set G = ^^^(I * ()),^^^(((I,u) -TermEval) . mm),()____;
A2: dom () = AllTermsOf S by FUNCT_2:def 1;
^^^(I * ()),^^^(((I,u) -TermEval) . mm),()____ is Function of (),U by Lm4;
then A3: dom ^^^(I * ()),^^^(((I,u) -TermEval) . mm),()____ = AllTermsOf S by FUNCT_2:def 1;
A4: (((I,u) -TermEval) . (mm + 1)) . t = ^^^(I * ()),^^^(((I,u) -TermEval) . mm),()____ . t by Def7
.= ((I * ()) . t) . (^^^(((I,u) -TermEval) . mm),()__ . t) by
.= ((I * ()) . t) . ((((I,u) -TermEval) . mm) * (() . tt)) by
.= ((I * ()) . t) . ((((I,u) -TermEval) . mm) * ()) by FOMODEL1:def 39
.= (I . (() . t)) . ((((I,u) -TermEval) . mm) * ()) by ;
hence (((I,u) -TermEval) . (mm + 1)) . t = (I . (() . t)) . ((((I,u) -TermEval) . mm) * ()) ; :: thesis: ( t is 0 -termal implies (((I,u) -TermEval) . (mm + 1)) . t = (I . (() . t)) . {} )
assume t is 0 -termal ; :: thesis: (((I,u) -TermEval) . (mm + 1)) . t = (I . (() . t)) . {}
then reconsider tt = t as 0 -termal string of S ;
reconsider s = () . tt as literal Element of S ;
reconsider v = I . s as Interpreter of s,U ;
(((I,u) -TermEval) . (mm + 1)) . t = v . {} by A4;
hence (((I,u) -TermEval) . (mm + 1)) . t = (I . (() . t)) . {} ; :: thesis: verum