let S be Language; 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 . ((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 ; 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; 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; 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; 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 ; ( (((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))
; ( t is 0 -termal implies (((I,u) -TermEval) . (mm + 1)) . t = (I . ((S -firstChar) . t)) . {} )
assume
t is 0 -termal
; (((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)) . {}
; verum