let U be non empty set ; 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 b2,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; for S being Language
for l1, l2 being literal Element of S
for phi0 being 0wff string of S
for I being b1,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; 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; 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; 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; ( 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
; ((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
;
per cases
( r <> TheEqSymbOf S or r = TheEqSymbOf S )
;
suppose A9:
r <> TheEqSymbOf S
;
((l1,u) ReassignIn I) -AtomicEval phi0 = ((l2,u) ReassignIn I) -AtomicEval ((l1,l2) -SymbolSubstIn phi0)then ((l1,u) ReassignIn I) -AtomicEval phi0 =
(((l2,u) ReassignIn I) . r2) . ((((l2,u) ReassignIn I) -TermEval) * (SubTerms psi0))
by FOMODEL2:14, A8, A1, A2
.=
((l2,u) ReassignIn I) -AtomicEval psi0
by FOMODEL2:14, A9, A1
;
hence
((l1,u) ReassignIn I) -AtomicEval phi0 = ((l2,u) ReassignIn I) -AtomicEval ((l1,l2) -SymbolSubstIn phi0)
;
verum end;