let X be set ; :: thesis: for S being Language holds ((S,X) -freeInterpreter) -TermEval = id (AllTermsOf S)

let S be Language; :: thesis: ((S,X) -freeInterpreter) -TermEval = id (AllTermsOf S)

set u = the Element of AllTermsOf S;

set I = (S,X) -freeInterpreter ;

set TE = (((S,X) -freeInterpreter), the Element of AllTermsOf S) -TermEval ;

set T = S -termsOfMaxDepth ;

set F = S -firstChar ;

set SS = AllSymbolsOf S;

set TT = AllTermsOf S;

reconsider Tf = S -termsOfMaxDepth as Function ;

reconsider LH = ((S,X) -freeInterpreter) -TermEval , RH = id (AllTermsOf S) as Function of (AllTermsOf S),(AllTermsOf S) ;

let S be Language; :: thesis: ((S,X) -freeInterpreter) -TermEval = id (AllTermsOf S)

set u = the Element of AllTermsOf S;

set I = (S,X) -freeInterpreter ;

set TE = (((S,X) -freeInterpreter), the Element of AllTermsOf S) -TermEval ;

set T = S -termsOfMaxDepth ;

set F = S -firstChar ;

set SS = AllSymbolsOf S;

set TT = AllTermsOf S;

reconsider Tf = S -termsOfMaxDepth as Function ;

reconsider LH = ((S,X) -freeInterpreter) -TermEval , RH = id (AllTermsOf S) as Function of (AllTermsOf S),(AllTermsOf S) ;

now :: thesis: for tt being Element of AllTermsOf S holds LH . tt = RH . tt

hence
((S,X) -freeInterpreter) -TermEval = id (AllTermsOf S)
by FUNCT_2:63; :: thesis: verumlet tt be Element of AllTermsOf S; :: thesis: LH . tt = RH . tt

consider mm being Element of NAT such that

A1: tt in Tf . mm by FOMODEL1:5;

reconsider ttt = tt as Element of (S -termsOfMaxDepth) . mm by A1;

reconsider M = mm + 1 as Element of NAT ;

reconsider tttt = tt as Element of (S -termsOfMaxDepth) . mm by A1;

set uv = ((S,X) -freeInterpreter) -TermEval tt;

((((S,X) -freeInterpreter), the Element of AllTermsOf S) -TermEval) . M is Element of Funcs ((AllTermsOf S),(AllTermsOf S)) ;

then reconsider f = ((((S,X) -freeInterpreter), the Element of AllTermsOf S) -TermEval) . (mm + 1) as Function of (AllTermsOf S),(AllTermsOf S) ;

((f | ((S -termsOfMaxDepth) . mm)) . ttt) \+\ (f . ttt) = {} ;

then A2: (f | ((S -termsOfMaxDepth) . mm)) . ttt = f . ttt by FOMODEL0:29;

A3: ( (id ((S -termsOfMaxDepth) . mm)) . tttt = tttt & (id (AllTermsOf S)) . tt = tt ) ;

thus LH . tt = ((S,X) -freeInterpreter) -TermEval tt by FOMODEL2:def 10

.= f . tt by FOMODEL2:def 9, A1

.= RH . tt by A3, A2, Lm28 ; :: thesis: verum

end;consider mm being Element of NAT such that

A1: tt in Tf . mm by FOMODEL1:5;

reconsider ttt = tt as Element of (S -termsOfMaxDepth) . mm by A1;

reconsider M = mm + 1 as Element of NAT ;

reconsider tttt = tt as Element of (S -termsOfMaxDepth) . mm by A1;

set uv = ((S,X) -freeInterpreter) -TermEval tt;

((((S,X) -freeInterpreter), the Element of AllTermsOf S) -TermEval) . M is Element of Funcs ((AllTermsOf S),(AllTermsOf S)) ;

then reconsider f = ((((S,X) -freeInterpreter), the Element of AllTermsOf S) -TermEval) . (mm + 1) as Function of (AllTermsOf S),(AllTermsOf S) ;

((f | ((S -termsOfMaxDepth) . mm)) . ttt) \+\ (f . ttt) = {} ;

then A2: (f | ((S -termsOfMaxDepth) . mm)) . ttt = f . ttt by FOMODEL0:29;

A3: ( (id ((S -termsOfMaxDepth) . mm)) . tttt = tttt & (id (AllTermsOf S)) . tt = tt ) ;

thus LH . tt = ((S,X) -freeInterpreter) -TermEval tt by FOMODEL2:def 10

.= f . tt by FOMODEL2:def 9, A1

.= RH . tt by A3, A2, Lm28 ; :: thesis: verum