let S be Language; :: thesis: for U being non empty set
for phi being 0wff string of S
for I being S,b₁ -interpreter-like Function holds
( ( (S -firstChar) . phi <> TheEqSymbOf S implies I -AtomicEval phi = (I . ((S -firstChar) . phi)) . ((I -TermEval) * (SubTerms phi)) ) & ( (S -firstChar) . phi = TheEqSymbOf S implies I -AtomicEval phi = (U -deltaInterpreter) . ((I -TermEval) * (SubTerms phi)) ) )
let U be non empty set ; :: thesis: for phi being 0wff string of S
for I being S,U -interpreter-like Function holds
( ( (S -firstChar) . phi <> TheEqSymbOf S implies I -AtomicEval phi = (I . ((S -firstChar) . phi)) . ((I -TermEval) * (SubTerms phi)) ) & ( (S -firstChar) . phi = TheEqSymbOf S implies I -AtomicEval phi = (U -deltaInterpreter) . ((I -TermEval) * (SubTerms phi)) ) )
let phi be 0wff string of S; :: thesis: for I being S,U -interpreter-like Function holds
( ( (S -firstChar) . phi <> TheEqSymbOf S implies I -AtomicEval phi = (I . ((S -firstChar) . phi)) . ((I -TermEval) * (SubTerms phi)) ) & ( (S -firstChar) . phi = TheEqSymbOf S implies I -AtomicEval phi = (U -deltaInterpreter) . ((I -TermEval) * (SubTerms phi)) ) )
let I be S,U -interpreter-like Function; :: thesis: ( ( (S -firstChar) . phi <> TheEqSymbOf S implies I -AtomicEval phi = (I . ((S -firstChar) . phi)) . ((I -TermEval) * (SubTerms phi)) ) & ( (S -firstChar) . phi = TheEqSymbOf S implies I -AtomicEval phi = (U -deltaInterpreter) . ((I -TermEval) * (SubTerms phi)) ) )
set TT = AllTermsOf S;
set E = TheEqSymbOf S;
set p = SubTerms phi;
set F = S -firstChar ;
set r = (S -firstChar) . phi;
set n = |.(ar ((S -firstChar) . phi)).|;
set AF = AtomicFormulasOf S;
set d = U -deltaInterpreter ;
set p = SubTerms phi;
set V = I -AtomicEval phi;
set f = (I ===) . ((S -firstChar) . phi);
set UV = I -TermEval ;
set G = I . ((S -firstChar) . phi);
A1: |.(ar (TheEqSymbOf S)).| - 2 = 0 ;
thus ( (S -firstChar) . phi <> TheEqSymbOf S implies I -AtomicEval phi = (I . ((S -firstChar) . phi)) . ((I -TermEval) * (SubTerms phi)) ) :: thesis: ( (S -firstChar) . phi = TheEqSymbOf S implies I -AtomicEval phi = (U -deltaInterpreter) . ((I -TermEval) * (SubTerms phi)) )

proof

assume (S -firstChar) . phi <> TheEqSymbOf S ; :: thesis: I -AtomicEval phi = (I . ((S -firstChar) . phi)) . ((I -TermEval) * (SubTerms phi))
then not (S -firstChar) . phi in dom ((TheEqSymbOf S) .--> (U -deltaInterpreter)) by TARSKI:def 1;
hence I -AtomicEval phi = (I . ((S -firstChar) . phi)) . ((I -TermEval) * (SubTerms phi)) by FUNCT_4:11; :: thesis: verum

end;

assume (S -firstChar) . phi = TheEqSymbOf S ; :: thesis: I -AtomicEval phi = (U -deltaInterpreter) . ((I -TermEval) * (SubTerms phi))
then A2: ( (S -firstChar) . phi in {(TheEqSymbOf S)} & |.(ar ((S -firstChar) . phi)).| = 2 ) by TARSKI:def 1, A1;
then (S -firstChar) . phi in dom ((TheEqSymbOf S) .--> (U -deltaInterpreter)) ;
then (I ===) . ((S -firstChar) . phi) = ((TheEqSymbOf S) .--> (U -deltaInterpreter)) . ((S -firstChar) . phi) by FUNCT_4:13
.= U -deltaInterpreter by A2, FUNCOP_1:7 ;
hence I -AtomicEval phi = (U -deltaInterpreter) . ((I -TermEval) * (SubTerms phi)) ; :: thesis: verum