let X be set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: (((((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 = abs (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) | ((abs (ar ((S -firstChar) . t))) -tuples_on (AllTermsOf S));
reconsider f = X -freeInterpreter ((S -firstChar) . t) as Function of ((abs (ar ((S -firstChar) . t))) -tuples_on (AllTermsOf S)),(AllTermsOf S) by FOMODEL2:def 2;
B1: (((S -firstChar) . t) -compound) | ((abs (ar ((S -firstChar) . t))) -tuples_on (AllTermsOf S)) = f by DefFreeInt1;
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 B0: {} in dom ((((S -firstChar) . t) -compound) | ((abs (ar ((S -firstChar) . t))) -tuples_on (AllTermsOf S))) by B1, TARSKI:def 1;
thus (((((S,X) -freeInterpreter),tt) -TermEval) . (m + 1)) . t = (((S,X) -freeInterpreter) . ((S -firstChar) . t)) . {} by FOMODEL2:3
.= f . {} by DefFree1
.= ((((S -firstChar) . t) -compound) | ((abs (ar ((S -firstChar) . t))) -tuples_on (AllTermsOf S))) . {} by DefFreeInt1
.= (((S -firstChar) . t) -compound) . {} by B0, FUNCT_1:47
.= ((S -firstChar) . t) -compound E by DefCompound1
.= <*((S -firstChar) . t)*> null {}
.= t by FOMODEL2:1 ; :: thesis: verum