let S be Language; :: thesis: for U being non empty set
for t being termal string of S
for I being S,b1 -interpreter-like Function holds () . t = (I . (() . t)) . (() * ())

let U be non empty set ; :: thesis: for t being termal string of S
for I being S,U -interpreter-like Function holds () . t = (I . (() . t)) . (() * ())

let t be termal string of S; :: thesis: for I being S,U -interpreter-like Function holds () . t = (I . (() . t)) . (() * ())
let I be S,U -interpreter-like Function; :: thesis: () . t = (I . (() . t)) . (() * ())
set u = the Element of U;
set TI = I -TermEval ;
set TII = (I, the Element of U) -TermEval ;
set TT = AllTermsOf S;
set F = S -firstChar ;
set s = () . t;
set m = Depth t;
set T = S -termsOfMaxDepth ;
set ST = SubTerms t;
reconsider mm = Depth t, MM = () + 1 as Element of NAT by ORDINAL1:def 12;
A1: t is (Depth t) + (0 * 1) -termal by FOMODEL1:def 40;
reconsider tm = t as Depth t -termal string of S by FOMODEL1:def 40;
reconsider tM = t as mm + 1 -termal string of S by A1;
reconsider Tm = () . mm, TM = () . MM as Subset of () by FOMODEL1:2;
reconsider ttt = tm as Element of () . mm by FOMODEL1:def 33;
reconsider tt = t as Element of AllTermsOf S by FOMODEL1:def 32;
set V = I -TermEval tt;
reconsider IM = ((I, the Element of U) -TermEval) . MM as Function of (),U ;
SubTerms tM is Tm -valued ;
then A2: ( dom (() | Tm) = Tm & dom (IM | Tm) = Tm & rng () c= Tm ) by ;
() . t = I -TermEval tt by Def9
.= (((I, the Element of U) -TermEval) . MM) . ttt by Def8
.= (((I, the Element of U) -TermEval) . ((() + 1) + 1)) . tm by Lm6
.= (I . (() . t)) . ((((I, the Element of U) -TermEval) . MM) * ()) by Th3
.= (I . (() . t)) . (((((I, the Element of U) -TermEval) . MM) | Tm) * ()) by
.= (I . (() . t)) . ((() | Tm) * ()) by Th20
.= (I . (() . t)) . (() * ()) by ;
hence (I -TermEval) . t = (I . (() . t)) . (() * ()) ; :: thesis: verum