let X be set ; :: thesis: for U being non empty set
for S being Language
for l being literal Element of S
for I being b₂,b₁ -interpreter-like Function
for tt being Element of AllTermsOf S holds (I -TermEval) * (((l,tt) ReassignIn ((S,X) -freeInterpreter)) -TermEval) = ((l,((I -TermEval) . tt)) ReassignIn I) -TermEval
let U be non empty set ; :: thesis: for S being Language
for l being literal Element of S
for I being b₁,U -interpreter-like Function
for tt being Element of AllTermsOf S holds (I -TermEval) * (((l,tt) ReassignIn ((S,X) -freeInterpreter)) -TermEval) = ((l,((I -TermEval) . tt)) ReassignIn I) -TermEval
let S be Language; :: thesis: for l being literal Element of S
for I being S,U -interpreter-like Function
for tt being Element of AllTermsOf S holds (I -TermEval) * (((l,tt) ReassignIn ((S,X) -freeInterpreter)) -TermEval) = ((l,((I -TermEval) . tt)) ReassignIn I) -TermEval
let l be literal Element of S; :: thesis: for I being S,U -interpreter-like Function
for tt being Element of AllTermsOf S holds (I -TermEval) * (((l,tt) ReassignIn ((S,X) -freeInterpreter)) -TermEval) = ((l,((I -TermEval) . tt)) ReassignIn I) -TermEval
let I be S,U -interpreter-like Function; :: thesis: for tt being Element of AllTermsOf S holds (I -TermEval) * (((l,tt) ReassignIn ((S,X) -freeInterpreter)) -TermEval) = ((l,((I -TermEval) . tt)) ReassignIn I) -TermEval
let tt be Element of AllTermsOf S; :: thesis: (I -TermEval) * (((l,tt) ReassignIn ((S,X) -freeInterpreter)) -TermEval) = ((l,((I -TermEval) . tt)) ReassignIn I) -TermEval
set TI = I -TermEval ;
set u = (I -TermEval) . tt;
set J = (l,((I -TermEval) . tt)) ReassignIn I;
set TJ = ((l,((I -TermEval) . tt)) ReassignIn I) -TermEval ;
set F = S -firstChar ;
set C = S -multiCat ;
set FI = (S,X) -freeInterpreter ;
set FJ = (l,tt) ReassignIn ((S,X) -freeInterpreter);
set TF = ((l,tt) ReassignIn ((S,X) -freeInterpreter)) -TermEval ;
set TT = AllTermsOf S;
set T = S -termsOfMaxDepth ;
reconsider LH = (I -TermEval) * (((l,tt) ReassignIn ((S,X) -freeInterpreter)) -TermEval), RH = ((l,((I -TermEval) . tt)) ReassignIn I) -TermEval as Function of (AllTermsOf S),U ;

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

let tt0 be Element of AllTermsOf S; :: thesis: LH . tt0 = RH . tt0
reconsider t = tt0 as termal string of S ;
set n = Depth t;
reconsider nn = Depth t, NN = (Depth t) + 1 as Element of NAT by ORDINAL1:def 12;
reconsider tn = t as Depth t -termal string of S by FOMODEL1:def 40;
tn is (Depth t) + (0 * 1) -termal ;
then reconsider tN = tn as NN -termal string of S ;
reconsider TN = (S -termsOfMaxDepth) . NN, Tn = (S -termsOfMaxDepth) . nn as Subset of (AllTermsOf S) by FOMODEL1:2;
reconsider tnn = tn as Element of Tn by FOMODEL1:def 33;
reconsider tNN = tN as Element of TN by FOMODEL1:def 33;
((((l,tt) ReassignIn ((S,X) -freeInterpreter)),tt) -TermEval) . NN is Element of Funcs ((AllTermsOf S),(AllTermsOf S)) ;
then reconsider FJN = ((((l,tt) ReassignIn ((S,X) -freeInterpreter)),tt) -TermEval) . NN as Function of (AllTermsOf S),(AllTermsOf S) ;
((((l,((I -TermEval) . tt)) ReassignIn I),((I -TermEval) . tt)) -TermEval) . NN is Element of Funcs ((AllTermsOf S),U) ;
then reconsider JN = ((((l,((I -TermEval) . tt)) ReassignIn I),((I -TermEval) . tt)) -TermEval) . NN as Function of (AllTermsOf S),U ;
( ((I -TermEval) . (FJN . tt0)) \+\ (((I -TermEval) * FJN) . tt0) = {} & ((((I -TermEval) * FJN) | TN) . tNN) \+\ (((I -TermEval) * FJN) . tNN) = {} & ((JN | TN) . tNN) \+\ (JN . tNN) = {} ) ;
then A1: ( ((I -TermEval) * FJN) . tt0 = (I -TermEval) . (FJN . tt0) & (((I -TermEval) * FJN) | TN) . tt0 = ((I -TermEval) * FJN) . tt0 & (JN | TN) . tt0 = JN . tt0 ) by FOMODEL0:29;
(LH . tt0) \+\ ((I -TermEval) . ((((l,tt) ReassignIn ((S,X) -freeInterpreter)) -TermEval) . tt0)) = {} ;
then LH . tt0 = (I -TermEval) . ((((l,tt) ReassignIn ((S,X) -freeInterpreter)) -TermEval) . tt0) by FOMODEL0:29
.= (I -TermEval) . (((l,tt) ReassignIn ((S,X) -freeInterpreter)) -TermEval tt0) by FOMODEL2:def 10
.= (I -TermEval) . (FJN . tnn) by FOMODEL2:def 9
.= (((((l,((I -TermEval) . tt)) ReassignIn I),((I -TermEval) . tt)) -TermEval) . NN) . tnn by A1, Th7
.= ((l,((I -TermEval) . tt)) ReassignIn I) -TermEval tt0 by FOMODEL2:def 9
.= (((l,((I -TermEval) . tt)) ReassignIn I) -TermEval) . tt0 by FOMODEL2:def 10 ;
hence LH . tt0 = RH . tt0 ; :: thesis: verum

end;

hence (I -TermEval) * (((l,tt) ReassignIn ((S,X) -freeInterpreter)) -TermEval) = ((l,((I -TermEval) . tt)) ReassignIn I) -TermEval by FUNCT_2:63; :: thesis: verum