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₄ -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₃ -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₂ -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₁ -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 ;
B2: ( dom Jj = OwnSymbolsOf S & dom jJ = OwnSymbolsOf S ) by DefQuot3, PARTFUN1:def 2;
set jJ = j quotient E;
set g = l .--> ({{}} --> u);
set h = {{}} --> u;
set G = l .--> ({{}} --> X);
reconsider n = abs (ar l) as Nat ;
B3: ( {{}} = 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;
Z0: ( dom (l .--> ({{}} --> u)) = {l} & dom (l .--> ({{}} --> X)) = {l} ) by FUNCOP_1:13;
then B0: ( dom (l .--> ({{}} --> u)) = {l} & dom (l .--> ({{}} --> X)) = {l} & l in dom (l .--> ({{}} --> u)) & l in dom (l .--> ({{}} --> X)) ) by TARSKI:def 1;
B4: ( n -placesOf E = Enn & dom (E -class) = U & dom ({{}} --> ((E -class) . u)) = {{}} & dom ({{}} --> u) = {{}} & (id {{}}) \+\ ({} .--> {}) = {} ) by Lm33, FUNCT_2:def 1;
then B1: ( n -placesOf E = Enn & u in dom (E -class) & {} in dom ({{}} --> ((E -class) . u)) & id {{}} = {} .--> {} ) by FOMODEL0:29, TARSKI:def 1;
{} in dom ({{}} --> u) by B4, TARSKI:def 1;
then reconsider hh = {{}} --> u as Enn,E -respecting Function by Lm25;
reconsider hhh = hh as n -placesOf E,E -respecting Function of (n -tuples_on U),U by B3, B4;

now

let s be set ; :: thesis: ( s in OwnSymbolsOf S implies Jj . b₁ = (j quotient E) . b₁ )
assume s in OwnSymbolsOf S ; :: thesis: Jj . b₁ = (j quotient E) . b₁
then reconsider ss = s as own Element of S ;

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

suppose D0: s in dom (l .--> ({{}} --> X)) ; :: thesis: Jj . b₁ = (j quotient E) . b₁

D1: s = l by D0, Z0, TARSKI:def 1;
then D2: (j quotient E) . s = (j . l) quotient E by DefQuot3b
.= (n -tuple2Class E) * ((j . l) quotient ((n -placesOf E),E)) by DefQuot2
.= (n -tuple2Class E) * (((l .--> ({{}} --> u)) . l) quotient ((n -placesOf E),E)) by B0, FUNCT_4:13
.= (n -tuple2Class E) * (({{}} --> u) quotient ((n -placesOf E),E)) by FUNCOP_1:72
.= (n -placesOf ((E -class) ~)) * ((E -class) * hhh) by Lm24
.= (id {{}}) * ((E -class) * hhh) by Lm33
.= ({{}} --> ((E -class) . u)) * ({{}} --> {}) by B1, FUNCOP_1:17
.= {{}} --> (({} .--> ((E -class) . u)) . {}) by B1, FUNCOP_1:17
.= {{}} --> X by FUNCOP_1:72 ;
Jj . s = (l .--> ({{}} --> X)) . l by D0, D1, FUNCT_4:13
.= {{}} --> X by FUNCOP_1:72 ;
hence Jj . s = (j quotient E) . s by D2; :: thesis: verum

end;

suppose D0: not s in dom (l .--> ({{}} --> X)) ; :: thesis: Jj . b₁ = (j quotient E) . b₁

then Jj . s = I . s by FUNCT_4:11
.= (i . ss) quotient E by DefQuot3b
.= (j . ss) quotient E by D0, Z0, FUNCT_4:11
.= (j quotient E) . ss by DefQuot3b ;
hence Jj . s = (j quotient E) . s ; :: thesis: verum

end;

end;

end;

hence (l,((E -class) . u)) ReassignIn (i quotient E) = ((l,u) ReassignIn i) quotient E by B2, FUNCT_1:2; :: thesis: verum