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 b4 -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 b3 -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 b2 -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 b1 -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;
now :: thesis: for s being object st s in OwnSymbolsOf S holds
Jj . s = (j quotient E) . s
let s be object ; :: thesis: ( s in OwnSymbolsOf S implies Jj . b1 = (j quotient E) . b1 )
assume s in OwnSymbolsOf S ; :: thesis: Jj . b1 = (j quotient E) . b1
then reconsider ss = s as own Element of S ;
per cases ( s in dom (l .--> ({{}} --> X)) or not s in dom (l .--> ({{}} --> X)) ) ;
suppose A6: s in dom (l .--> ({{}} --> X)) ; :: thesis: Jj . b1 = (j quotient E) . b1
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;
suppose A9: not s in dom (l .--> ({{}} --> X)) ; :: thesis: Jj . b1 = (j quotient E) . b1
then Jj . s = I . s by FUNCT_4:11
.= (i . ss) quotient E by Def18
.= (j . ss) quotient E by A9, 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