let U1 be non empty set ; for S being Language
for R being Equivalence_Relation of U1
for phi being 0wff string of S
for i being b1,U1 -interpreter-like b2 -respecting Function st (S -firstChar) . phi <> TheEqSymbOf S holds
(i quotient R) -AtomicEval phi = i -AtomicEval phi
let S be Language; for R being Equivalence_Relation of U1
for phi being 0wff string of S
for i being S,U1 -interpreter-like b1 -respecting Function st (S -firstChar) . phi <> TheEqSymbOf S holds
(i quotient R) -AtomicEval phi = i -AtomicEval phi
let R be Equivalence_Relation of U1; 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; 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; ( (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 = abs (ar ((S -firstChar) . phi));
set U = Class R;
set I = i quotient R;
set UV = (i quotient R) -TermEval ;
set N1 = (abs (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 ;
Z0:
( SubTerms phi in (abs (ar ((S -firstChar) . phi))) -tuples_on (AllTermsOf S) & dom ((abs (ar ((S -firstChar) . phi))) -placesOf ((R -class) * (i -TermEval))) = (abs (ar ((S -firstChar) . phi))) -tuples_on (AllTermsOf S) & dom ((abs (ar ((S -firstChar) . phi))) -placesOf (i -TermEval)) = (abs (ar ((S -firstChar) . phi))) -tuples_on (AllTermsOf S) )
by FOMODEL0:16, FUNCT_2:def 1;
assume C0:
(S -firstChar) . phi <> TheEqSymbOf S
; (i quotient R) -AtomicEval phi = i -AtomicEval phi
then C1: (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 Lm32
.=
((i quotient R) . ((S -firstChar) . phi)) . (((abs (ar ((S -firstChar) . phi))) -placesOf ((R -class) * (i -TermEval))) . (SubTerms phi))
by Lm22
.=
(((i quotient R) . ((S -firstChar) . phi)) * ((abs (ar ((S -firstChar) . phi))) -placesOf ((R -class) * (i -TermEval)))) . (SubTerms phi)
by Z0, FUNCT_1:13
;
reconsider o = (S -firstChar) . phi as Element of OwnSymbolsOf S by C0, FOMODEL1:15;
set gg = i . o;
set GG = (i quotient R) . o;
reconsider ggg = i . o as (abs (ar ((S -firstChar) . phi))) -placesOf R, id BOOLEAN -respecting Function of ((abs (ar ((S -firstChar) . phi))) -tuples_on U1),BOOLEAN by DefCompatible2, FOMODEL2:def 2;
set F = ggg quotient (((abs (ar ((S -firstChar) . phi))) -placesOf R),(id BOOLEAN));
reconsider P = peeler BOOLEAN as Function ;
reconsider nuisance1 = ggg quotient (((abs (ar ((S -firstChar) . phi))) -placesOf R),(id BOOLEAN)), nuisance2 = (abs (ar ((S -firstChar) . phi))) -tuple2Class R, nuisance3 = P as Relation ;
reconsider RR = R -class as Relation of U1,(Class R) ;
Z2: (i quotient R) . o =
(i . o) quotient R
by DefQuot3b
.=
(peeler BOOLEAN) * ((ggg quotient (((abs (ar ((S -firstChar) . phi))) -placesOf R),(id BOOLEAN))) * ((abs (ar ((S -firstChar) . phi))) -tuple2Class R))
by DefQuot2
;
C4:
((abs (ar ((S -firstChar) . phi))) -tuple2Class R) * ((abs (ar ((S -firstChar) . phi))) -placesOf ((R -class) * (i -TermEval))) = (((abs (ar ((S -firstChar) . phi))) -placesOf R) -class) * ((abs (ar ((S -firstChar) . phi))) -placesOf (i -TermEval))
(P * ((ggg quotient (((abs (ar ((S -firstChar) . phi))) -placesOf R),(id BOOLEAN))) * ((abs (ar ((S -firstChar) . phi))) -tuple2Class R))) * ((abs (ar ((S -firstChar) . phi))) -placesOf ((R -class) * (i -TermEval))) =
P * (((ggg quotient (((abs (ar ((S -firstChar) . phi))) -placesOf R),(id BOOLEAN))) * ((abs (ar ((S -firstChar) . phi))) -tuple2Class R)) * ((abs (ar ((S -firstChar) . phi))) -placesOf ((R -class) * (i -TermEval))))
by RELAT_1:36
.=
P * ((ggg quotient (((abs (ar ((S -firstChar) . phi))) -placesOf R),(id BOOLEAN))) * ((((abs (ar ((S -firstChar) . phi))) -placesOf R) -class) * ((abs (ar ((S -firstChar) . phi))) -placesOf (i -TermEval))))
by C4, RELAT_1:36
;
then (i quotient R) -AtomicEval phi =
(P * (((ggg quotient (((abs (ar ((S -firstChar) . phi))) -placesOf R),(id BOOLEAN))) * (((abs (ar ((S -firstChar) . phi))) -placesOf R) -class)) * ((abs (ar ((S -firstChar) . phi))) -placesOf (i -TermEval)))) . (SubTerms phi)
by C1, Z2, RELAT_1:36
.=
((P * ((ggg quotient (((abs (ar ((S -firstChar) . phi))) -placesOf R),(id BOOLEAN))) * (((abs (ar ((S -firstChar) . phi))) -placesOf R) -class))) * ((abs (ar ((S -firstChar) . phi))) -placesOf (i -TermEval))) . (SubTerms phi)
by RELAT_1:36
.=
(P * ((ggg quotient (((abs (ar ((S -firstChar) . phi))) -placesOf R),(id BOOLEAN))) * (((abs (ar ((S -firstChar) . phi))) -placesOf R) -class))) . (((abs (ar ((S -firstChar) . phi))) -placesOf (i -TermEval)) . (SubTerms phi))
by Z0, FUNCT_1:13
.=
(P * ((ggg quotient (((abs (ar ((S -firstChar) . phi))) -placesOf R),(id BOOLEAN))) * (((abs (ar ((S -firstChar) . phi))) -placesOf R) -class))) . ((i -TermEval) * (SubTerms phi))
by Lm22
.=
(P * (((id BOOLEAN) -class) * ggg)) . ((i -TermEval) * (SubTerms phi))
by Lm27
.=
((P * ((id BOOLEAN) -class)) * ggg) . ((i -TermEval) * (SubTerms phi))
by RELAT_1:36
.=
((id BOOLEAN) * ggg) . ((i -TermEval) * (SubTerms phi))
by Lm26
.=
ggg . ((i -TermEval) * (SubTerms phi))
by FUNCT_2:17
.=
i -AtomicEval phi
by FOMODEL2:14
;
hence
(i quotient R) -AtomicEval phi = i -AtomicEval phi
; verum