let S be Language; :: thesis: for U being non empty set
for u being Element of U
for I being S,b₁ -interpreter-like Function
for t being termal string of S
for mm being Element of NAT holds
( (((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)) . {} ) )
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 . ((S -firstChar) . t)) . ((((I,u) -TermEval) . mm) * (SubTerms t)) & ( t is 0 -termal implies (((I,u) -TermEval) . (mm + 1)) . t = (I . ((S -firstChar) . 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 . ((S -firstChar) . t)) . ((((I,u) -TermEval) . mm) * (SubTerms t)) & ( t is 0 -termal implies (((I,u) -TermEval) . (mm + 1)) . t = (I . ((S -firstChar) . 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 . ((S -firstChar) . t)) . ((((I,u) -TermEval) . mm) * (SubTerms t)) & ( t is 0 -termal implies (((I,u) -TermEval) . (mm + 1)) . t = (I . ((S -firstChar) . t)) . {} ) )
let t be termal string of S; :: thesis: for mm being Element of NAT holds
( (((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)) . {} ) )
let mm be Element of NAT ; :: thesis: ( (((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)) . {} ) )
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 * (S -firstChar)) ) by FOMODEL1:def 32, Lm4;
reconsider tt = t as Element of AllTermsOf S by FOMODEL1:def 32;
set G = ^^^(I * (S -firstChar)),^^^(((I,u) -TermEval) . mm),(S -subTerms)____;
A2: dom (S -subTerms) = AllTermsOf S by FUNCT_2:def 1;
^^^(I * (S -firstChar)),^^^(((I,u) -TermEval) . mm),(S -subTerms)____ is Function of (AllTermsOf S),U by Lm4;
then A3: dom ^^^(I * (S -firstChar)),^^^(((I,u) -TermEval) . mm),(S -subTerms)____ = AllTermsOf S by FUNCT_2:def 1;
A4: (((I,u) -TermEval) . (mm + 1)) . t = ^^^(I * (S -firstChar)),^^^(((I,u) -TermEval) . mm),(S -subTerms)____ . t by Def7
.= ((I * (S -firstChar)) . t) . (^^^(((I,u) -TermEval) . mm),(S -subTerms)__ . t) by A3, A1, FOMODEL0:def 4
.= ((I * (S -firstChar)) . t) . ((((I,u) -TermEval) . mm) * ((S -subTerms) . tt)) by Def6, A2
.= ((I * (S -firstChar)) . t) . ((((I,u) -TermEval) . mm) * (SubTerms t)) by FOMODEL1:def 39
.= (I . ((S -firstChar) . t)) . ((((I,u) -TermEval) . mm) * (SubTerms t)) by A1, FUNCT_1:12 ;
hence (((I,u) -TermEval) . (mm + 1)) . t = (I . ((S -firstChar) . t)) . ((((I,u) -TermEval) . mm) * (SubTerms t)) ; :: thesis: ( t is 0 -termal implies (((I,u) -TermEval) . (mm + 1)) . t = (I . ((S -firstChar) . t)) . {} )
assume t is 0 -termal ; :: thesis: (((I,u) -TermEval) . (mm + 1)) . t = (I . ((S -firstChar) . t)) . {}
then reconsider tt = t as 0 -termal string of S ;
reconsider s = (S -firstChar) . 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 . ((S -firstChar) . t)) . {} ; :: thesis: verum