let U be non empty set ; :: thesis: for u being Element of U
for k being Nat
for S being Language
for E being Equivalence_Relation of U
for I being b₃,U -interpreter-like b₄ -respecting Function holds (((I quotient E),((E -class) . u)) -TermEval) . k = (E -class) * (((I,u) -TermEval) . k)
let u be Element of U; :: thesis: for k being Nat
for S being Language
for E being Equivalence_Relation of U
for I being b₂,U -interpreter-like b₃ -respecting Function holds (((I quotient E),((E -class) . u)) -TermEval) . k = (E -class) * (((I,u) -TermEval) . k)
let k be Nat; :: thesis: for S being Language
for E being Equivalence_Relation of U
for I being b₁,U -interpreter-like b₂ -respecting Function holds (((I quotient E),((E -class) . u)) -TermEval) . k = (E -class) * (((I,u) -TermEval) . k)
let S be Language; :: thesis: for E being Equivalence_Relation of U
for I being S,U -interpreter-like b₁ -respecting Function holds (((I quotient E),((E -class) . u)) -TermEval) . k = (E -class) * (((I,u) -TermEval) . k)
let E be Equivalence_Relation of U; :: thesis: for I being S,U -interpreter-like E -respecting Function holds (((I quotient E),((E -class) . u)) -TermEval) . k = (E -class) * (((I,u) -TermEval) . k)
reconsider e = (E -class) . u as Element of Class E ;
let I be S,U -interpreter-like E -respecting Function; :: thesis: (((I quotient E),((E -class) . u)) -TermEval) . k = (E -class) * (((I,u) -TermEval) . k)
set te = (I,u) -TermEval ;
set II = I quotient E;
set TE = ((I quotient E),e) -TermEval ;
set F = S -firstChar ;
set O = OwnSymbolsOf S;
set TT = AllTermsOf S;
defpred S₁[ Nat] means (((I quotient E),e) -TermEval) . $1 = (E -class) * (((I,u) -TermEval) . $1);
B0: S₁[ 0 ]

proof

B0: ( (((I quotient E),e) -TermEval) . 0 = (AllTermsOf S) --> e & ((I,u) -TermEval) . 0 = (AllTermsOf S) --> u ) by FOMODEL2:def 8;
dom (E -class) = U by FUNCT_2:def 1;
hence S₁[ 0 ] by B0, FUNCOP_1:17; :: thesis: verum

end;

B1: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume B0: S₁[m] ; :: thesis: S₁[m + 1]
reconsider mm = m, MM = m + 1 as Element of NAT by ORDINAL1:def 12;
( ((I,u) -TermEval) . mm is Element of Funcs ((AllTermsOf S),U) & ((I,u) -TermEval) . MM is Element of Funcs ((AllTermsOf S),U) ) ;
then reconsider tm = ((I,u) -TermEval) . mm, tmm = ((I,u) -TermEval) . MM as Function of (AllTermsOf S),U ;
( (((I quotient E),e) -TermEval) . mm is Element of Funcs ((AllTermsOf S),(Class E)) & (((I quotient E),e) -TermEval) . MM is Element of Funcs ((AllTermsOf S),(Class E)) ) ;
then reconsider TM = (((I quotient E),e) -TermEval) . mm, TMM = (((I quotient E),e) -TermEval) . MM as Function of (AllTermsOf S),(Class E) ;

now

let tt be Element of AllTermsOf S; :: thesis: TMM . tt = ((E -class) * tmm) . tt
reconsider t = tt as termal string of S ;
set s = (S -firstChar) . t;
set g = I . ((S -firstChar) . t);
set G = (I quotient E) . ((S -firstChar) . t);
set sub = SubTerms t;
set n = abs (ar ((S -firstChar) . t));
reconsider gg = I . ((S -firstChar) . t) as (abs (ar ((S -firstChar) . t))) -placesOf E,E -respecting Function of ((abs (ar ((S -firstChar) . t))) -tuples_on U),U by FOMODEL2:def 2;
B1: (I . ((S -firstChar) . t)) quotient E = (gg quotient (((abs (ar ((S -firstChar) . t))) -placesOf E),E)) * ((abs (ar ((S -firstChar) . t))) -tuple2Class E) by DefQuot2;
reconsider ggg = gg quotient (((abs (ar ((S -firstChar) . t))) -placesOf E),E) as Function ;
Z2: ( tm * (SubTerms t) is U -valued abs (ar ((S -firstChar) . t)) -element FinSequence & dom ((abs (ar ((S -firstChar) . t))) -placesOf (E -class)) = (abs (ar ((S -firstChar) . t))) -tuples_on U & dom gg = (abs (ar ((S -firstChar) . t))) -tuples_on U & dom tmm = AllTermsOf S ) by FUNCT_2:def 1;
thus TMM . tt = ((I quotient E) . ((S -firstChar) . t)) . (((((I quotient E),e) -TermEval) . m) * (SubTerms t)) by FOMODEL2:3
.= ((I . ((S -firstChar) . t)) quotient E) . (((((I quotient E),e) -TermEval) . m) * (SubTerms t)) by DefQuot3b
.= ((I . ((S -firstChar) . t)) quotient E) . ((E -class) * (tm * (SubTerms t))) by B0, RELAT_1:36
.= ((I . ((S -firstChar) . t)) quotient E) . (((abs (ar ((S -firstChar) . t))) -placesOf (E -class)) . (tm * (SubTerms t))) by Lm22
.= ((ggg * ((abs (ar ((S -firstChar) . t))) -tuple2Class E)) * ((abs (ar ((S -firstChar) . t))) -placesOf (E -class))) . (tm * (SubTerms t)) by B1, Z2, FOMODEL0:16, FUNCT_1:13
.= (ggg * (((abs (ar ((S -firstChar) . t))) -tuple2Class E) * ((abs (ar ((S -firstChar) . t))) -placesOf (E -class)))) . (tm * (SubTerms t)) by RELAT_1:36
.= (ggg * (((abs (ar ((S -firstChar) . t))) -placesOf E) -class)) . (tm * (SubTerms t)) by Lm23
.= ((E -class) * gg) . (tm * (SubTerms t)) by Lm27
.= (E -class) . (gg . (tm * (SubTerms t))) by Z2, FOMODEL0:16, FUNCT_1:13
.= (E -class) . ((((I,u) -TermEval) . (m + 1)) . t) by FOMODEL2:3
.= ((E -class) * tmm) . tt by Z2, FUNCT_1:13 ; :: thesis: verum

end;

hence S₁[m + 1] by FUNCT_2:63; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(B0, B1);
hence (((I quotient E),((E -class) . u)) -TermEval) . k = (E -class) * (((I,u) -TermEval) . k) ; :: thesis: verum