let S be Language; :: thesis: for U being non empty set

for t being termal string of S

for I being S,b_{1} -interpreter-like Function holds (I -TermEval) . t = (I . ((S -firstChar) . t)) . ((I -TermEval) * (SubTerms t))

let U be non empty set ; :: thesis: for t being termal string of S

for I being S,U -interpreter-like Function holds (I -TermEval) . t = (I . ((S -firstChar) . t)) . ((I -TermEval) * (SubTerms t))

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

let I be S,U -interpreter-like Function; :: thesis: (I -TermEval) . t = (I . ((S -firstChar) . t)) . ((I -TermEval) * (SubTerms 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 = (S -firstChar) . t;

set m = Depth t;

set T = S -termsOfMaxDepth ;

set ST = SubTerms t;

reconsider mm = Depth t, MM = (Depth t) + 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 = (S -termsOfMaxDepth) . mm, TM = (S -termsOfMaxDepth) . MM as Subset of (AllTermsOf S) by FOMODEL1:2;

reconsider ttt = tm as Element of (S -termsOfMaxDepth) . 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 (AllTermsOf S),U ;

SubTerms tM is Tm -valued ;

then A2: ( dom ((I -TermEval) | Tm) = Tm & dom (IM | Tm) = Tm & rng (SubTerms t) c= Tm ) by RELAT_1:def 19, PARTFUN1:def 2;

(I -TermEval) . t = I -TermEval tt by Def9

.= (((I, the Element of U) -TermEval) . MM) . ttt by Def8

.= (((I, the Element of U) -TermEval) . (((Depth t) + 1) + 1)) . tm by Lm6

.= (I . ((S -firstChar) . t)) . ((((I, the Element of U) -TermEval) . MM) * (SubTerms t)) by Th3

.= (I . ((S -firstChar) . t)) . (((((I, the Element of U) -TermEval) . MM) | Tm) * (SubTerms t)) by RELAT_1:165, A2

.= (I . ((S -firstChar) . t)) . (((I -TermEval) | Tm) * (SubTerms t)) by Th20

.= (I . ((S -firstChar) . t)) . ((I -TermEval) * (SubTerms t)) by A2, RELAT_1:165 ;

hence (I -TermEval) . t = (I . ((S -firstChar) . t)) . ((I -TermEval) * (SubTerms t)) ; :: thesis: verum

for t being termal string of S

for I being S,b

let U be non empty set ; :: thesis: for t being termal string of S

for I being S,U -interpreter-like Function holds (I -TermEval) . t = (I . ((S -firstChar) . t)) . ((I -TermEval) * (SubTerms t))

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

let I be S,U -interpreter-like Function; :: thesis: (I -TermEval) . t = (I . ((S -firstChar) . t)) . ((I -TermEval) * (SubTerms 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 = (S -firstChar) . t;

set m = Depth t;

set T = S -termsOfMaxDepth ;

set ST = SubTerms t;

reconsider mm = Depth t, MM = (Depth t) + 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 = (S -termsOfMaxDepth) . mm, TM = (S -termsOfMaxDepth) . MM as Subset of (AllTermsOf S) by FOMODEL1:2;

reconsider ttt = tm as Element of (S -termsOfMaxDepth) . 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 (AllTermsOf S),U ;

SubTerms tM is Tm -valued ;

then A2: ( dom ((I -TermEval) | Tm) = Tm & dom (IM | Tm) = Tm & rng (SubTerms t) c= Tm ) by RELAT_1:def 19, PARTFUN1:def 2;

(I -TermEval) . t = I -TermEval tt by Def9

.= (((I, the Element of U) -TermEval) . MM) . ttt by Def8

.= (((I, the Element of U) -TermEval) . (((Depth t) + 1) + 1)) . tm by Lm6

.= (I . ((S -firstChar) . t)) . ((((I, the Element of U) -TermEval) . MM) * (SubTerms t)) by Th3

.= (I . ((S -firstChar) . t)) . (((((I, the Element of U) -TermEval) . MM) | Tm) * (SubTerms t)) by RELAT_1:165, A2

.= (I . ((S -firstChar) . t)) . (((I -TermEval) | Tm) * (SubTerms t)) by Th20

.= (I . ((S -firstChar) . t)) . ((I -TermEval) * (SubTerms t)) by A2, RELAT_1:165 ;

hence (I -TermEval) . t = (I . ((S -firstChar) . t)) . ((I -TermEval) * (SubTerms t)) ; :: thesis: verum