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 ;
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 = abs (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} ) by FUNCOP_1:13;
then A4: ( dom (l .--> ({{}} --> u)) = {l} & dom (l .--> ({{}} --> X)) = {l} & l in dom (l .--> ({{}} --> u)) & l in dom (l .--> ({{}} --> X)) ) by TARSKI:def 1;
A5: ( n -placesOf E = Enn & dom (E -class) = U & dom ({{}} --> ((E -class) . u)) = {{}} & dom ({{}} --> u) = {{}} & (id {{}}) \+\ ({} .--> {}) = {} ) by Lm30, FUNCT_2:def 1;
then A6: ( 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 A5, 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, A5;

now :: thesis: for s being set st s in OwnSymbolsOf S holds
Jj . s = (j quotient E) . s

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 A7: s in dom (l .--> ({{}} --> X)) ; :: thesis: Jj . b₁ = (j quotient E) . b₁

A8: s = l by A7, TARSKI:def 1;
then A9: (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 A4, 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 A6, FUNCOP_1:17
.= {{}} --> (({} .--> ((E -class) . u)) . {}) by A6, FUNCOP_1:17
.= {{}} --> X by FUNCOP_1:72 ;
Jj . s = (l .--> ({{}} --> X)) . l by A7, A8, FUNCT_4:13
.= {{}} --> X by FUNCOP_1:72 ;
hence Jj . s = (j quotient E) . s by A9; :: thesis: verum

end;

suppose A10: 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 Def18
.= (j . ss) quotient E by A10, A3, FUNCT_4:11
.= (j quotient E) . ss by Def18 ;
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 A1, FUNCT_1:2; :: thesis: verum