let U be non empty set ; :: thesis: for S being Language
for l being literal Element of S
for phi0 being 0wff string of S
for I being b₁,U -interpreter-like Function
for tt being Element of AllTermsOf S holds I -AtomicEval ((l,tt) AtomicSubst phi0) = ((l,((I -TermEval) . tt)) ReassignIn I) -AtomicEval phi0
let S be Language; :: thesis: for l being literal Element of S
for phi0 being 0wff string of S
for I being S,U -interpreter-like Function
for tt being Element of AllTermsOf S holds I -AtomicEval ((l,tt) AtomicSubst phi0) = ((l,((I -TermEval) . tt)) ReassignIn I) -AtomicEval phi0
let l be literal Element of S; :: thesis: for phi0 being 0wff string of S
for I being S,U -interpreter-like Function
for tt being Element of AllTermsOf S holds I -AtomicEval ((l,tt) AtomicSubst phi0) = ((l,((I -TermEval) . tt)) ReassignIn I) -AtomicEval phi0
let phi0 be 0wff string of S; :: thesis: for I being S,U -interpreter-like Function
for tt being Element of AllTermsOf S holds I -AtomicEval ((l,tt) AtomicSubst phi0) = ((l,((I -TermEval) . tt)) ReassignIn I) -AtomicEval phi0
let I be S,U -interpreter-like Function; :: thesis: for tt being Element of AllTermsOf S holds I -AtomicEval ((l,tt) AtomicSubst phi0) = ((l,((I -TermEval) . tt)) ReassignIn I) -AtomicEval phi0
let tt be Element of AllTermsOf S; :: thesis: I -AtomicEval ((l,tt) AtomicSubst phi0) = ((l,((I -TermEval) . tt)) ReassignIn I) -AtomicEval phi0
set psi0 = (l,tt) AtomicSubst phi0;
set u = (I -TermEval) . tt;
set J = (l,((I -TermEval) . tt)) ReassignIn I;
set F = S -firstChar ;
set C = S -multiCat ;
set FI = (S,{}) -freeInterpreter ;
set s1 = (S -firstChar) . phi0;
set s2 = (S -firstChar) . ((l,tt) AtomicSubst phi0);
set n1 = abs (ar ((S -firstChar) . phi0));
set n2 = abs (ar ((S -firstChar) . ((l,tt) AtomicSubst phi0)));
set TI = I -TermEval ;
set TJ = ((l,((I -TermEval) . tt)) ReassignIn I) -TermEval ;
set E = TheEqSymbOf S;
set FJ = (l,tt) ReassignIn ((S,{}) -freeInterpreter);
set d = U -deltaInterpreter ;
not (S -firstChar) . phi0 in {l} by TARSKI:def 1;
then not (S -firstChar) . phi0 in dom (l .--> ({} .--> ((I -TermEval) . tt))) by FUNCOP_1:13;
then C0: ( (S -firstChar) . phi0 = (S -firstChar) . ((l,tt) AtomicSubst phi0) & ((l,((I -TermEval) . tt)) ReassignIn I) . ((S -firstChar) . phi0) = I . ((S -firstChar) . phi0) ) by Lm42, FUNCT_4:11;
C1: (I -TermEval) * (SubTerms ((l,tt) AtomicSubst phi0)) = (I -TermEval) * ((((l,tt) ReassignIn ((S,{}) -freeInterpreter)) -TermEval) * (SubTerms phi0)) by Lm42
.= ((I -TermEval) * (((l,tt) ReassignIn ((S,{}) -freeInterpreter)) -TermEval)) * (SubTerms phi0) by RELAT_1:36
.= (((l,((I -TermEval) . tt)) ReassignIn I) -TermEval) * (SubTerms phi0) by Lm43 ;

per cases ( (S -firstChar) . ((l,tt) AtomicSubst phi0) <> TheEqSymbOf S or (S -firstChar) . ((l,tt) AtomicSubst phi0) = TheEqSymbOf S ) ;

suppose D0: (S -firstChar) . ((l,tt) AtomicSubst phi0) <> TheEqSymbOf S ; :: thesis: I -AtomicEval ((l,tt) AtomicSubst phi0) = ((l,((I -TermEval) . tt)) ReassignIn I) -AtomicEval phi0

then I -AtomicEval ((l,tt) AtomicSubst phi0) = (((l,((I -TermEval) . tt)) ReassignIn I) . ((S -firstChar) . phi0)) . ((((l,((I -TermEval) . tt)) ReassignIn I) -TermEval) * (SubTerms phi0)) by C0, C1, FOMODEL2:14
.= ((l,((I -TermEval) . tt)) ReassignIn I) -AtomicEval phi0 by D0, C0, FOMODEL2:14 ;
hence I -AtomicEval ((l,tt) AtomicSubst phi0) = ((l,((I -TermEval) . tt)) ReassignIn I) -AtomicEval phi0 ; :: thesis: verum

end;

suppose D0: (S -firstChar) . ((l,tt) AtomicSubst phi0) = TheEqSymbOf S ; :: thesis: I -AtomicEval ((l,tt) AtomicSubst phi0) = ((l,((I -TermEval) . tt)) ReassignIn I) -AtomicEval phi0

then I -AtomicEval ((l,tt) AtomicSubst phi0) = (U -deltaInterpreter) . ((I -TermEval) * (SubTerms ((l,tt) AtomicSubst phi0))) by FOMODEL2:14
.= ((l,((I -TermEval) . tt)) ReassignIn I) -AtomicEval phi0 by D0, C0, C1, FOMODEL2:14 ;
hence I -AtomicEval ((l,tt) AtomicSubst phi0) = ((l,((I -TermEval) . tt)) ReassignIn I) -AtomicEval phi0 ; :: thesis: verum

end;

end;