let U be non empty set ; :: thesis: for u being Element of U

for S being Language

for l being literal Element of S

for E being Equivalence_Relation of U

for i being b_{4} -respecting Element of U -InterpretersOf S holds (l,((E -class) . u)) ReassignIn (i quotient E) = ((l,u) ReassignIn i) quotient E

let u be Element of U; :: thesis: for S being Language

for l being literal Element of S

for E being Equivalence_Relation of U

for i being b_{3} -respecting Element of U -InterpretersOf S holds (l,((E -class) . u)) ReassignIn (i quotient E) = ((l,u) ReassignIn i) quotient E

let S be Language; :: thesis: for l being literal Element of S

for E being Equivalence_Relation of U

for i being b_{2} -respecting Element of U -InterpretersOf S holds (l,((E -class) . u)) ReassignIn (i quotient E) = ((l,u) ReassignIn i) quotient E

let l be literal Element of S; :: thesis: for E being Equivalence_Relation of U

for i being b_{1} -respecting Element of U -InterpretersOf S holds (l,((E -class) . u)) ReassignIn (i quotient E) = ((l,u) ReassignIn i) quotient E

set II = U -InterpretersOf S;

let E be Equivalence_Relation of U; :: thesis: for i being E -respecting Element of U -InterpretersOf S holds (l,((E -class) . u)) ReassignIn (i quotient E) = ((l,u) ReassignIn i) quotient E

let i be E -respecting Element of U -InterpretersOf S; :: thesis: (l,((E -class) . u)) ReassignIn (i quotient E) = ((l,u) ReassignIn i) quotient E

set x = u;

set O = OwnSymbolsOf S;

set UU = Class E;

set III = (Class E) -InterpretersOf S;

reconsider X = (E -class) . u as Element of Class E ;

reconsider I = i quotient E as Element of (Class E) -InterpretersOf S ;

reconsider j = (l,u) ReassignIn i as Element of U -InterpretersOf S ;

reconsider Jj = (l,X) ReassignIn I as Element of (Class E) -InterpretersOf S ;

reconsider jJ = j quotient E as Function ;

A1: ( dom Jj = OwnSymbolsOf S & dom jJ = OwnSymbolsOf S ) by Def17, PARTFUN1:def 2;

set jJ = j quotient E;

set g = l .--> ({{}} --> u);

set h = {{}} --> u;

set G = l .--> ({{}} --> X);

reconsider n = |.(ar l).| as Nat ;

A2: ( {{}} = 0 -tuples_on U & id {{}} is Equivalence_Relation of {{}} ) by FOMODEL0:10;

then reconsider Enn = id {{}} as Equivalence_Relation of (0 -tuples_on U) ;

set En = n -placesOf E;

set nE = n -tuple2Class E;

A3: ( dom (l .--> ({{}} --> u)) = {l} & dom (l .--> ({{}} --> X)) = {l} & l in dom (l .--> ({{}} --> u)) & l in dom (l .--> ({{}} --> X)) ) by TARSKI:def 1;

A4: ( n -placesOf E = Enn & dom (E -class) = U & dom ({{}} --> ((E -class) . u)) = {{}} & dom ({{}} --> u) = {{}} & (id {{}}) \+\ ({} .--> {}) = {} ) by Lm30, FUNCT_2:def 1;

then A5: ( n -placesOf E = Enn & u in dom (E -class) & {} in dom ({{}} --> ((E -class) . u)) & id {{}} = {} .--> {} ) by TARSKI:def 1, FOMODEL0:29;

{} in dom ({{}} --> u) by TARSKI:def 1;

then reconsider hh = {{}} --> u as Enn,E -respecting Function by Lm22;

reconsider hhh = hh as n -placesOf E,E -respecting Function of (n -tuples_on U),U by A2, A4;

for S being Language

for l being literal Element of S

for E being Equivalence_Relation of U

for i being b

let u be Element of U; :: thesis: for S being Language

for l being literal Element of S

for E being Equivalence_Relation of U

for i being b

let S be Language; :: thesis: for l being literal Element of S

for E being Equivalence_Relation of U

for i being b

let l be literal Element of S; :: thesis: for E being Equivalence_Relation of U

for i being b

set II = U -InterpretersOf S;

let E be Equivalence_Relation of U; :: thesis: for i being E -respecting Element of U -InterpretersOf S holds (l,((E -class) . u)) ReassignIn (i quotient E) = ((l,u) ReassignIn i) quotient E

let i be E -respecting Element of U -InterpretersOf S; :: thesis: (l,((E -class) . u)) ReassignIn (i quotient E) = ((l,u) ReassignIn i) quotient E

set x = u;

set O = OwnSymbolsOf S;

set UU = Class E;

set III = (Class E) -InterpretersOf S;

reconsider X = (E -class) . u as Element of Class E ;

reconsider I = i quotient E as Element of (Class E) -InterpretersOf S ;

reconsider j = (l,u) ReassignIn i as Element of U -InterpretersOf S ;

reconsider Jj = (l,X) ReassignIn I as Element of (Class E) -InterpretersOf S ;

reconsider jJ = j quotient E as Function ;

A1: ( dom Jj = OwnSymbolsOf S & dom jJ = OwnSymbolsOf S ) by Def17, PARTFUN1:def 2;

set jJ = j quotient E;

set g = l .--> ({{}} --> u);

set h = {{}} --> u;

set G = l .--> ({{}} --> X);

reconsider n = |.(ar l).| as Nat ;

A2: ( {{}} = 0 -tuples_on U & id {{}} is Equivalence_Relation of {{}} ) by FOMODEL0:10;

then reconsider Enn = id {{}} as Equivalence_Relation of (0 -tuples_on U) ;

set En = n -placesOf E;

set nE = n -tuple2Class E;

A3: ( dom (l .--> ({{}} --> u)) = {l} & dom (l .--> ({{}} --> X)) = {l} & l in dom (l .--> ({{}} --> u)) & l in dom (l .--> ({{}} --> X)) ) by TARSKI:def 1;

A4: ( n -placesOf E = Enn & dom (E -class) = U & dom ({{}} --> ((E -class) . u)) = {{}} & dom ({{}} --> u) = {{}} & (id {{}}) \+\ ({} .--> {}) = {} ) by Lm30, FUNCT_2:def 1;

then A5: ( n -placesOf E = Enn & u in dom (E -class) & {} in dom ({{}} --> ((E -class) . u)) & id {{}} = {} .--> {} ) by TARSKI:def 1, FOMODEL0:29;

{} in dom ({{}} --> u) by TARSKI:def 1;

then reconsider hh = {{}} --> u as Enn,E -respecting Function by Lm22;

reconsider hhh = hh as n -placesOf E,E -respecting Function of (n -tuples_on U),U by A2, A4;

now :: thesis: for s being object st s in OwnSymbolsOf S holds

Jj . s = (j quotient E) . s

hence
(l,((E -class) . u)) ReassignIn (i quotient E) = ((l,u) ReassignIn i) quotient E
by A1, FUNCT_1:2; :: thesis: verumJj . s = (j quotient E) . s

let s be object ; :: thesis: ( s in OwnSymbolsOf S implies Jj . b_{1} = (j quotient E) . b_{1} )

assume s in OwnSymbolsOf S ; :: thesis: Jj . b_{1} = (j quotient E) . b_{1}

then reconsider ss = s as own Element of S ;

end;assume s in OwnSymbolsOf S ; :: thesis: Jj . b

then reconsider ss = s as own Element of S ;

per cases
( s in dom (l .--> ({{}} --> X)) or not s in dom (l .--> ({{}} --> X)) )
;

end;

suppose A6:
s in dom (l .--> ({{}} --> X))
; :: thesis: Jj . b_{1} = (j quotient E) . b_{1}

A7:
s = l
by A6, TARSKI:def 1;

then A8: (j quotient E) . s = (j . l) quotient E by Def18

.= (n -tuple2Class E) * ((j . l) quotient ((n -placesOf E),E)) by Def15

.= (n -tuple2Class E) * (((l .--> ({{}} --> u)) . l) quotient ((n -placesOf E),E)) by A3, FUNCT_4:13

.= (n -tuple2Class E) * (({{}} --> u) quotient ((n -placesOf E),E)) by FUNCOP_1:72

.= (n -placesOf ((E -class) ~)) * ((E -class) * hhh) by Lm21

.= (id {{}}) * ((E -class) * hhh) by Lm30

.= ({{}} --> ((E -class) . u)) * ({{}} --> {}) by FUNCOP_1:17, A5

.= {{}} --> (({} .--> ((E -class) . u)) . {}) by FUNCOP_1:17, A5

.= {{}} --> X by FUNCOP_1:72 ;

Jj . s = (l .--> ({{}} --> X)) . l by A6, A7, FUNCT_4:13

.= {{}} --> X by FUNCOP_1:72 ;

hence Jj . s = (j quotient E) . s by A8; :: thesis: verum

end;then A8: (j quotient E) . s = (j . l) quotient E by Def18

.= (n -tuple2Class E) * ((j . l) quotient ((n -placesOf E),E)) by Def15

.= (n -tuple2Class E) * (((l .--> ({{}} --> u)) . l) quotient ((n -placesOf E),E)) by A3, FUNCT_4:13

.= (n -tuple2Class E) * (({{}} --> u) quotient ((n -placesOf E),E)) by FUNCOP_1:72

.= (n -placesOf ((E -class) ~)) * ((E -class) * hhh) by Lm21

.= (id {{}}) * ((E -class) * hhh) by Lm30

.= ({{}} --> ((E -class) . u)) * ({{}} --> {}) by FUNCOP_1:17, A5

.= {{}} --> (({} .--> ((E -class) . u)) . {}) by FUNCOP_1:17, A5

.= {{}} --> X by FUNCOP_1:72 ;

Jj . s = (l .--> ({{}} --> X)) . l by A6, A7, FUNCT_4:13

.= {{}} --> X by FUNCOP_1:72 ;

hence Jj . s = (j quotient E) . s by A8; :: thesis: verum