let U be non empty set ; :: thesis: for u being Element of U
for S being Language
for l1, l2 being literal Element of S
for phi0 being 0wff string of S
for I being b₂,U -interpreter-like Function st phi0 is (AllSymbolsOf S) \ {l2} -valued holds
((l1,u) ReassignIn I) -AtomicEval phi0 = ((l2,u) ReassignIn I) -AtomicEval ((l1,l2) -SymbolSubstIn phi0)
let u be Element of U; :: thesis: for S being Language
for l1, l2 being literal Element of S
for phi0 being 0wff string of S
for I being b₁,U -interpreter-like Function st phi0 is (AllSymbolsOf S) \ {l2} -valued holds
((l1,u) ReassignIn I) -AtomicEval phi0 = ((l2,u) ReassignIn I) -AtomicEval ((l1,l2) -SymbolSubstIn phi0)
let S be Language; :: thesis: for l1, l2 being literal Element of S
for phi0 being 0wff string of S
for I being S,U -interpreter-like Function st phi0 is (AllSymbolsOf S) \ {l2} -valued holds
((l1,u) ReassignIn I) -AtomicEval phi0 = ((l2,u) ReassignIn I) -AtomicEval ((l1,l2) -SymbolSubstIn phi0)
let l1, l2 be literal Element of S; :: thesis: for phi0 being 0wff string of S
for I being S,U -interpreter-like Function st phi0 is (AllSymbolsOf S) \ {l2} -valued holds
((l1,u) ReassignIn I) -AtomicEval phi0 = ((l2,u) ReassignIn I) -AtomicEval ((l1,l2) -SymbolSubstIn phi0)
let phi0 be 0wff string of S; :: thesis: for I being S,U -interpreter-like Function st phi0 is (AllSymbolsOf S) \ {l2} -valued holds
((l1,u) ReassignIn I) -AtomicEval phi0 = ((l2,u) ReassignIn I) -AtomicEval ((l1,l2) -SymbolSubstIn phi0)
let I be S,U -interpreter-like Function; :: thesis: ( phi0 is (AllSymbolsOf S) \ {l2} -valued implies ((l1,u) ReassignIn I) -AtomicEval phi0 = ((l2,u) ReassignIn I) -AtomicEval ((l1,l2) -SymbolSubstIn phi0) )
set I1 = (l1,u) ReassignIn I;
set I2 = (l2,u) ReassignIn I;
set s = l1 SubstWith l2;
set E1 = ((l1,u) ReassignIn I) -TermEval ;
set E2 = ((l2,u) ReassignIn I) -TermEval ;
set T = S -termsOfMaxDepth ;
set TT = AllTermsOf S;
set SS = AllSymbolsOf S;
set F = S -firstChar ;
set C = S -multiCat ;
set g1 = l1 .--> ({} .--> u);
set g2 = l2 .--> ({} .--> u);
set L = LettersOf S;
set E = TheEqSymbOf S;
set d = U -deltaInterpreter ;
set SSS = (AllSymbolsOf S) \ {l2};
reconsider SSSS = (AllSymbolsOf S) \ {l2} as non empty Subset of (AllSymbolsOf S) ;
reconsider psi0 = (l1,l2) -SymbolSubstIn phi0 as 0wff string of S ;
reconsider r = (S -firstChar) . phi0, r2 = (S -firstChar) . psi0 as relational Element of S ;
phi0 . 1 = r by FOMODEL0:6;
then A1: r = psi0 . 1 by FUNCT_4:105
.= r2 by FOMODEL0:6 ;
( not r in dom (l1 .--> ({} .--> u)) & not r in dom (l2 .--> ({} .--> u)) ) by TARSKI:def 1;
then A2: ( ((l1,u) ReassignIn I) . r = I . r & ((l2,u) ReassignIn I) . r = I . r ) by FUNCT_4:11;
( dom (((l1,u) ReassignIn I) -TermEval) = AllTermsOf S & dom (((l2,u) ReassignIn I) -TermEval) = AllTermsOf S ) by FUNCT_2:def 1;
then A3: ( dom ((((l1,u) ReassignIn I) -TermEval) | (((AllSymbolsOf S) \ {l2}) *)) = (AllTermsOf S) /\ (((AllSymbolsOf S) \ {l2}) *) & dom ((l1 SubstWith l2) | (SSSS *)) = SSSS * ) by PARTFUN1:def 2, RELAT_1:61;
reconsider ST1 = SubTerms phi0 as Element of (AllTermsOf S) * ;
consider mm being Element of NAT such that
A4: SubTerms phi0 is Element of ((S -termsOfMaxDepth) . mm) * by Lm3;
reconsider Tm = (S -termsOfMaxDepth) . mm as non empty Subset of (AllTermsOf S) by FOMODEL1:2;
A5: dom ((((l1,u) ReassignIn I) -TermEval) | ((((AllSymbolsOf S) \ {l2}) *) /\ Tm)) = dom (((((l1,u) ReassignIn I) -TermEval) | (((AllSymbolsOf S) \ {l2}) *)) | Tm) by RELAT_1:71
.= (dom ((((l1,u) ReassignIn I) -TermEval) | (((AllSymbolsOf S) \ {l2}) *))) /\ Tm by RELAT_1:61
.= (Tm null (AllTermsOf S)) /\ (((AllSymbolsOf S) \ {l2}) *) by A3, XBOOLE_1:16
.= (((AllSymbolsOf S) \ {l2}) *) /\ Tm ;
A6: dom ((l1 SubstWith l2) | ((((AllSymbolsOf S) \ {l2}) *) /\ Tm)) = dom (((l1 SubstWith l2) | (((AllSymbolsOf S) \ {l2}) *)) | Tm) by RELAT_1:71
.= (((AllSymbolsOf S) \ {l2}) *) /\ Tm by A3, RELAT_1:61 ;
assume phi0 is (AllSymbolsOf S) \ {l2} -valued ; :: thesis: ((l1,u) ReassignIn I) -AtomicEval phi0 = ((l2,u) ReassignIn I) -AtomicEval ((l1,l2) -SymbolSubstIn phi0)
then reconsider R = rng phi0 as non empty Subset of SSSS by RELAT_1:def 19;
( rng (SubTerms phi0) c= R * & R * c= ((AllSymbolsOf S) \ {l2}) * ) by RELAT_1:def 19;
then A7: ( rng (SubTerms phi0) c= ((AllSymbolsOf S) \ {l2}) * & rng (SubTerms phi0) c= Tm ) by RELAT_1:def 19, A4;
A8: (((l1,u) ReassignIn I) -TermEval) * (SubTerms phi0) = ((((l1,u) ReassignIn I) -TermEval) | ((((AllSymbolsOf S) \ {l2}) *) /\ Tm)) * (SubTerms phi0) by A7, XBOOLE_1:19, A5, RELAT_1:165
.= (((((l2,u) ReassignIn I) -TermEval) * (l1 SubstWith l2)) | ((((AllSymbolsOf S) \ {l2}) *) /\ Tm)) * (SubTerms phi0) by Lm40
.= ((((l2,u) ReassignIn I) -TermEval) * ((l1 SubstWith l2) | ((((AllSymbolsOf S) \ {l2}) *) /\ Tm))) * (SubTerms phi0) by RELAT_1:83
.= (((l2,u) ReassignIn I) -TermEval) * (((l1 SubstWith l2) | ((((AllSymbolsOf S) \ {l2}) *) /\ Tm)) * (SubTerms phi0)) by RELAT_1:36
.= (((l2,u) ReassignIn I) -TermEval) * ((l1 SubstWith l2) * (SubTerms phi0)) by A7, XBOOLE_1:19, A6, RELAT_1:165
.= (((l2,u) ReassignIn I) -TermEval) * (SubTerms psi0) by Lm39 ;