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 = |.(ar ((S -firstChar) . phi0)).|;
set n2 = |.(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 dom (l .--> ({} .--> ((I -TermEval) . tt))) by TARSKI:def 1;
then A1: ( (S -firstChar) . phi0 = (S -firstChar) . ((l,tt) AtomicSubst phi0) & ((l,((I -TermEval) . tt)) ReassignIn I) . ((S -firstChar) . phi0) = I . ((S -firstChar) . phi0) ) by FUNCT_4:11, Lm36;
A2: (I -TermEval) * (SubTerms ((l,tt) AtomicSubst phi0)) = (I -TermEval) * ((((l,tt) ReassignIn ((S,{}) -freeInterpreter)) -TermEval) * (SubTerms phi0)) by Lm36
.= ((I -TermEval) * (((l,tt) ReassignIn ((S,{}) -freeInterpreter)) -TermEval)) * (SubTerms phi0) by RELAT_1:36
.= (((l,((I -TermEval) . tt)) ReassignIn I) -TermEval) * (SubTerms phi0) by Lm37 ;

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

suppose A3: (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 FOMODEL2:14, A1, A2
.= ((l,((I -TermEval) . tt)) ReassignIn I) -AtomicEval phi0 by FOMODEL2:14, A3, A1 ;
hence I -AtomicEval ((l,tt) AtomicSubst phi0) = ((l,((I -TermEval) . tt)) ReassignIn I) -AtomicEval phi0 ; :: thesis: verum

end;

suppose A4: (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 FOMODEL2:14, A4, A1, A2 ;
hence I -AtomicEval ((l,tt) AtomicSubst phi0) = ((l,((I -TermEval) . tt)) ReassignIn I) -AtomicEval phi0 ; :: thesis: verum

end;

end;