let U1 be non empty set ; :: thesis: for S being Language
for R being Equivalence_Relation of U1
for phi being 0wff string of S
for i being b₁,U1 -interpreter-like b₂ -respecting Function st (S -firstChar) . phi <> TheEqSymbOf S holds
(i quotient R) -AtomicEval phi = i -AtomicEval phi
let S be Language; :: thesis: for R being Equivalence_Relation of U1
for phi being 0wff string of S
for i being S,U1 -interpreter-like b₁ -respecting Function st (S -firstChar) . phi <> TheEqSymbOf S holds
(i quotient R) -AtomicEval phi = i -AtomicEval phi
let R be Equivalence_Relation of U1; :: thesis: for phi being 0wff string of S
for i being S,U1 -interpreter-like R -respecting Function st (S -firstChar) . phi <> TheEqSymbOf S holds
(i quotient R) -AtomicEval phi = i -AtomicEval phi
let phi be 0wff string of S; :: thesis: for i being S,U1 -interpreter-like R -respecting Function st (S -firstChar) . phi <> TheEqSymbOf S holds
(i quotient R) -AtomicEval phi = i -AtomicEval phi
let i be S,U1 -interpreter-like R -respecting Function; :: thesis: ( (S -firstChar) . phi <> TheEqSymbOf S implies (i quotient R) -AtomicEval phi = i -AtomicEval phi )
set TT = AllTermsOf S;
set E = TheEqSymbOf S;
set p = SubTerms phi;
set F = S -firstChar ;
set r = (S -firstChar) . phi;
set n = |.(ar ((S -firstChar) . phi)).|;
set U = Class R;
set I = i quotient R;
set UV = (i quotient R) -TermEval ;
set N1 = |.(ar ((S -firstChar) . phi)).| -tuples_on U1;
set V = (i quotient R) -AtomicEval phi;
set uv = i -TermEval ;
set v = i -AtomicEval phi;
set f = ((i quotient R) ===) . ((S -firstChar) . phi);
set G = (i quotient R) . ((S -firstChar) . phi);
set g = i . ((S -firstChar) . phi);
set d = (Class R) -deltaInterpreter ;
A1: ( SubTerms phi in |.(ar ((S -firstChar) . phi)).| -tuples_on (AllTermsOf S) & dom (|.(ar ((S -firstChar) . phi)).| -placesOf ((R -class) * (i -TermEval))) = |.(ar ((S -firstChar) . phi)).| -tuples_on (AllTermsOf S) & dom (|.(ar ((S -firstChar) . phi)).| -placesOf (i -TermEval)) = |.(ar ((S -firstChar) . phi)).| -tuples_on (AllTermsOf S) ) by FUNCT_2:def 1, FOMODEL0:16;
assume A2: (S -firstChar) . phi <> TheEqSymbOf S ; :: thesis: (i quotient R) -AtomicEval phi = i -AtomicEval phi
then A3: (i quotient R) -AtomicEval phi = ((i quotient R) . ((S -firstChar) . phi)) . (((i quotient R) -TermEval) * (SubTerms phi)) by FOMODEL2:14
.= ((i quotient R) . ((S -firstChar) . phi)) . (((R -class) * (i -TermEval)) * (SubTerms phi)) by Lm25
.= ((i quotient R) . ((S -firstChar) . phi)) . ((|.(ar ((S -firstChar) . phi)).| -placesOf ((R -class) * (i -TermEval))) . (SubTerms phi)) by Lm19
.= (((i quotient R) . ((S -firstChar) . phi)) * (|.(ar ((S -firstChar) . phi)).| -placesOf ((R -class) * (i -TermEval)))) . (SubTerms phi) by FUNCT_1:13, A1 ;
reconsider o = (S -firstChar) . phi as Element of OwnSymbolsOf S by A2, FOMODEL1:15;
set gg = i . o;
set GG = (i quotient R) . o;
reconsider ggg = i . o as |.(ar ((S -firstChar) . phi)).| -placesOf R, id BOOLEAN -respecting Function of (|.(ar ((S -firstChar) . phi)).| -tuples_on U1),BOOLEAN by FOMODEL2:def 2, Def10;
set F = ggg quotient ((|.(ar ((S -firstChar) . phi)).| -placesOf R),(id BOOLEAN));
reconsider P = peeler BOOLEAN as Function ;
reconsider nuisance1 = ggg quotient ((|.(ar ((S -firstChar) . phi)).| -placesOf R),(id BOOLEAN)), nuisance2 = |.(ar ((S -firstChar) . phi)).| -tuple2Class R, nuisance3 = P as Relation ;
reconsider RR = R -class as Relation of U1,(Class R) ;
A4: (i quotient R) . o = (i . o) quotient R by Def18
.= (peeler BOOLEAN) * ((ggg quotient ((|.(ar ((S -firstChar) . phi)).| -placesOf R),(id BOOLEAN))) * (|.(ar ((S -firstChar) . phi)).| -tuple2Class R)) by Def15 ;
A5: (|.(ar ((S -firstChar) . phi)).| -tuple2Class R) * (|.(ar ((S -firstChar) . phi)).| -placesOf ((R -class) * (i -TermEval))) = ((|.(ar ((S -firstChar) . phi)).| -placesOf R) -class) * (|.(ar ((S -firstChar) . phi)).| -placesOf (i -TermEval)) (P * ((ggg quotient ((|.(ar ((S -firstChar) . phi)).| -placesOf R),(id BOOLEAN))) * (|.(ar ((S -firstChar) . phi)).| -tuple2Class R))) * (|.(ar ((S -firstChar) . phi)).| -placesOf ((R -class) * (i -TermEval))) = P * (((ggg quotient ((|.(ar ((S -firstChar) . phi)).| -placesOf R),(id BOOLEAN))) * (|.(ar ((S -firstChar) . phi)).| -tuple2Class R)) * (|.(ar ((S -firstChar) . phi)).| -placesOf ((R -class) * (i -TermEval)))) by RELAT_1:36
.= P * ((ggg quotient ((|.(ar ((S -firstChar) . phi)).| -placesOf R),(id BOOLEAN))) * (((|.(ar ((S -firstChar) . phi)).| -placesOf R) -class) * (|.(ar ((S -firstChar) . phi)).| -placesOf (i -TermEval)))) by A5, RELAT_1:36 ;
then (i quotient R) -AtomicEval phi = (P * (((ggg quotient ((|.(ar ((S -firstChar) . phi)).| -placesOf R),(id BOOLEAN))) * ((|.(ar ((S -firstChar) . phi)).| -placesOf R) -class)) * (|.(ar ((S -firstChar) . phi)).| -placesOf (i -TermEval)))) . (SubTerms phi) by A3, A4, RELAT_1:36
.= ((P * ((ggg quotient ((|.(ar ((S -firstChar) . phi)).| -placesOf R),(id BOOLEAN))) * ((|.(ar ((S -firstChar) . phi)).| -placesOf R) -class))) * (|.(ar ((S -firstChar) . phi)).| -placesOf (i -TermEval))) . (SubTerms phi) by RELAT_1:36
.= (P * ((ggg quotient ((|.(ar ((S -firstChar) . phi)).| -placesOf R),(id BOOLEAN))) * ((|.(ar ((S -firstChar) . phi)).| -placesOf R) -class))) . ((|.(ar ((S -firstChar) . phi)).| -placesOf (i -TermEval)) . (SubTerms phi)) by FUNCT_1:13, A1
.= (P * ((ggg quotient ((|.(ar ((S -firstChar) . phi)).| -placesOf R),(id BOOLEAN))) * ((|.(ar ((S -firstChar) . phi)).| -placesOf R) -class))) . ((i -TermEval) * (SubTerms phi)) by Lm19
.= (P * (((id BOOLEAN) -class) * ggg)) . ((i -TermEval) * (SubTerms phi)) by Lm18
.= ((P * ((id BOOLEAN) -class)) * ggg) . ((i -TermEval) * (SubTerms phi)) by RELAT_1:36
.= ((id BOOLEAN) * ggg) . ((i -TermEval) * (SubTerms phi)) by Lm23
.= ggg . ((i -TermEval) * (SubTerms phi)) by FUNCT_2:17
.= i -AtomicEval phi by FOMODEL2:14 ;
hence (i quotient R) -AtomicEval phi = i -AtomicEval phi ; :: thesis: verum