let U be non empty set ; for S being Language
for E being Equivalence_Relation of U
for I being b1,U -interpreter-like b2 -respecting Function holds (I quotient E) -TermEval = (E -class) * (I -TermEval)
let S be Language; for E being Equivalence_Relation of U
for I being S,U -interpreter-like b1 -respecting Function holds (I quotient E) -TermEval = (E -class) * (I -TermEval)
let E be Equivalence_Relation of U; 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; (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 for tt being Element of AllTermsOf S holds ((I quotient E) -TermEval) . tt = ((E -class) * (I -TermEval)) . ttlet tt be
Element of
AllTermsOf S;
((I quotient E) -TermEval) . tt = ((E -class) * (I -TermEval)) . ttconsider 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
;
verum end;
hence
(I quotient E) -TermEval = (E -class) * (I -TermEval)
by FUNCT_2:63; verum