let U be non empty set ; :: thesis: for S being Language

for E being Equivalence_Relation of U

for I being b_{1},U -interpreter-like b_{2} -respecting Function holds (I quotient E) -TermEval = (E -class) * (I -TermEval)

let S be Language; :: thesis: for E being Equivalence_Relation of U

for I being S,U -interpreter-like b_{1} -respecting Function holds (I quotient E) -TermEval = (E -class) * (I -TermEval)

let E be Equivalence_Relation of U; :: thesis: for I being S,U -interpreter-like E -respecting Function holds (I quotient E) -TermEval = (E -class) * (I -TermEval)

set u = the Element of U;

let I be S,U -interpreter-like E -respecting Function; :: thesis: (I quotient E) -TermEval = (E -class) * (I -TermEval)

reconsider e = (E -class) . the Element of U as Element of Class E ;

set F = S -firstChar ;

set II = I quotient E;

set te = (I, the Element of U) -TermEval ;

set TE = ((I quotient E),e) -TermEval ;

set O = OwnSymbolsOf S;

set TT = AllTermsOf S;

set tee = I -TermEval ;

set TEE = (I quotient E) -TermEval ;

set T = S -termsOfMaxDepth ;

reconsider TF = S -termsOfMaxDepth as Function ;

for E being Equivalence_Relation of U

for I being b

let S be Language; :: thesis: for E being Equivalence_Relation of U

for I being S,U -interpreter-like b

let E be Equivalence_Relation of U; :: thesis: for I being S,U -interpreter-like E -respecting Function holds (I quotient E) -TermEval = (E -class) * (I -TermEval)

set u = the Element of U;

let I be S,U -interpreter-like E -respecting Function; :: thesis: (I quotient E) -TermEval = (E -class) * (I -TermEval)

reconsider e = (E -class) . the Element of U as Element of Class E ;

set F = S -firstChar ;

set II = I quotient E;

set te = (I, the Element of U) -TermEval ;

set TE = ((I quotient E),e) -TermEval ;

set O = OwnSymbolsOf S;

set TT = AllTermsOf S;

set tee = I -TermEval ;

set TEE = (I quotient E) -TermEval ;

set T = S -termsOfMaxDepth ;

reconsider TF = S -termsOfMaxDepth as Function ;

now :: thesis: for tt being Element of AllTermsOf S holds ((I quotient E) -TermEval) . tt = ((E -class) * (I -TermEval)) . tt

hence
(I quotient E) -TermEval = (E -class) * (I -TermEval)
by FUNCT_2:63; :: thesis: verumlet tt be Element of AllTermsOf S; :: thesis: ((I quotient E) -TermEval) . tt = ((E -class) * (I -TermEval)) . tt

consider mm being Element of NAT such that

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

set v = I -TermEval tt;

set V = (I quotient E) -TermEval tt;

reconsider MM = mm + 1 as Element of NAT ;

((I, the Element of U) -TermEval) . MM is Element of Funcs ((AllTermsOf S),U) ;

then A2: ( dom (((I, the Element of U) -TermEval) . MM) = AllTermsOf S & dom (I -TermEval) = AllTermsOf S ) by FUNCT_2:def 1;

thus ((I quotient E) -TermEval) . tt = (I quotient E) -TermEval tt by FOMODEL2:def 10

.= ((((I quotient E),e) -TermEval) . (mm + 1)) . tt by FOMODEL2:def 9, A1

.= ((E -class) * (((I, the Element of U) -TermEval) . (mm + 1))) . tt by Lm24

.= (E -class) . ((((I, the Element of U) -TermEval) . (mm + 1)) . tt) by FUNCT_1:13, A2

.= (E -class) . (I -TermEval tt) by FOMODEL2:def 9, A1

.= (E -class) . ((I -TermEval) . tt) by FOMODEL2:def 10

.= ((E -class) * (I -TermEval)) . tt by A2, FUNCT_1:13 ; :: thesis: verum

end;consider mm being Element of NAT such that

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

set v = I -TermEval tt;

set V = (I quotient E) -TermEval tt;

reconsider MM = mm + 1 as Element of NAT ;

((I, the Element of U) -TermEval) . MM is Element of Funcs ((AllTermsOf S),U) ;

then A2: ( dom (((I, the Element of U) -TermEval) . MM) = AllTermsOf S & dom (I -TermEval) = AllTermsOf S ) by FUNCT_2:def 1;

thus ((I quotient E) -TermEval) . tt = (I quotient E) -TermEval tt by FOMODEL2:def 10

.= ((((I quotient E),e) -TermEval) . (mm + 1)) . tt by FOMODEL2:def 9, A1

.= ((E -class) * (((I, the Element of U) -TermEval) . (mm + 1))) . tt by Lm24

.= (E -class) . ((((I, the Element of U) -TermEval) . (mm + 1)) . tt) by FUNCT_1:13, A2

.= (E -class) . (I -TermEval tt) by FOMODEL2:def 9, A1

.= (E -class) . ((I -TermEval) . tt) by FOMODEL2:def 10

.= ((E -class) * (I -TermEval)) . tt by A2, FUNCT_1:13 ; :: thesis: verum