let X be set ; for m being Nat
for S being Language
for tt being Element of AllTermsOf S
for t being 0 -termal string of S holds (((((S,X) -freeInterpreter),tt) -TermEval) . (m + 1)) . t = t
let m be Nat; for S being Language
for tt being Element of AllTermsOf S
for t being 0 -termal string of S holds (((((S,X) -freeInterpreter),tt) -TermEval) . (m + 1)) . t = t
let S be Language; for tt being Element of AllTermsOf S
for t being 0 -termal string of S holds (((((S,X) -freeInterpreter),tt) -TermEval) . (m + 1)) . t = t
let tt be Element of AllTermsOf S; for t being 0 -termal string of S holds (((((S,X) -freeInterpreter),tt) -TermEval) . (m + 1)) . t = t
let t be 0 -termal string of S; (((((S,X) -freeInterpreter),tt) -TermEval) . (m + 1)) . t = t
set I = (S,X) -freeInterpreter ;
set TT = AllTermsOf S;
set F = S -firstChar ;
set v = (S -firstChar) . t;
set n = |.(ar ((S -firstChar) . t)).|;
set C = S -multiCat ;
set II = (((S,X) -freeInterpreter),tt) -TermEval ;
set SS = AllSymbolsOf S;
set ff = (((S -firstChar) . t) -compound) | (|.(ar ((S -firstChar) . t)).| -tuples_on (AllTermsOf S));
reconsider f = X -freeInterpreter ((S -firstChar) . t) as Function of (|.(ar ((S -firstChar) . t)).| -tuples_on (AllTermsOf S)),(AllTermsOf S) by FOMODEL2:def 2;
A1:
(((S -firstChar) . t) -compound) | (|.(ar ((S -firstChar) . t)).| -tuples_on (AllTermsOf S)) = f
by Def3;
reconsider E = {} as Element of (((AllSymbolsOf S) *) \ {{}}) * by FINSEQ_1:49;
dom f = 0 -tuples_on (AllTermsOf S)
by FUNCT_2:def 1;
then
dom f = {{}}
by FOMODEL0:10;
then A2:
{} in dom ((((S -firstChar) . t) -compound) | (|.(ar ((S -firstChar) . t)).| -tuples_on (AllTermsOf S)))
by A1, TARSKI:def 1;
thus (((((S,X) -freeInterpreter),tt) -TermEval) . (m + 1)) . t =
(((S,X) -freeInterpreter) . ((S -firstChar) . t)) . {}
by FOMODEL2:3
.=
f . {}
by Def4
.=
((((S -firstChar) . t) -compound) | (|.(ar ((S -firstChar) . t)).| -tuples_on (AllTermsOf S))) . {}
by Def3
.=
(((S -firstChar) . t) -compound) . {}
by A2, FUNCT_1:47
.=
((S -firstChar) . t) -compound E
by Def2
.=
<*((S -firstChar) . t)*> null {}
.=
t
by FOMODEL2:1
; verum