let S be Language; :: thesis: for U being non empty set
for I being S,b₁ -interpreter-like Function
for phi being 0wff string of S st (S -firstChar) . phi = TheEqSymbOf S holds
( I -AtomicEval phi = 1 iff (I -TermEval) . ((SubTerms phi) . 1) = (I -TermEval) . ((SubTerms phi) . 2) )
let U be non empty set ; :: thesis: for I being S,U -interpreter-like Function
for phi being 0wff string of S st (S -firstChar) . phi = TheEqSymbOf S holds
( I -AtomicEval phi = 1 iff (I -TermEval) . ((SubTerms phi) . 1) = (I -TermEval) . ((SubTerms phi) . 2) )
let I be S,U -interpreter-like Function; :: thesis: for phi being 0wff string of S st (S -firstChar) . phi = TheEqSymbOf S holds
( I -AtomicEval phi = 1 iff (I -TermEval) . ((SubTerms phi) . 1) = (I -TermEval) . ((SubTerms phi) . 2) )
let phi be 0wff string of S; :: thesis: ( (S -firstChar) . phi = TheEqSymbOf S implies ( I -AtomicEval phi = 1 iff (I -TermEval) . ((SubTerms phi) . 1) = (I -TermEval) . ((SubTerms phi) . 2) ) )
set E = TheEqSymbOf S;
set p = SubTerms phi;
set F = S -firstChar ;
set s = (S -firstChar) . phi;
set UV = I -TermEval ;
set V = I -AtomicEval phi;
set d = U -deltaInterpreter ;
set U2 = 2 -tuples_on U;
set TT = AllTermsOf S;
set D = { <*u,u*> where u is Element of U : verum } ;
set n = |.(ar ((S -firstChar) . phi)).|;
A1: 2 -tuples_on U = { <*u1,u2*> where u1, u2 is Element of U : verum } by FINSEQ_2:99;
A2: |.(ar (TheEqSymbOf S)).| - 2 = 0 ;
reconsider r = (S -firstChar) . phi as relational Element of S ;
set f = (I ===) . r;
reconsider EE = TheEqSymbOf S as relational Element of S ;
assume A3: (S -firstChar) . phi = TheEqSymbOf S ; :: thesis: ( I -AtomicEval phi = 1 iff (I -TermEval) . ((SubTerms phi) . 1) = (I -TermEval) . ((SubTerms phi) . 2) )
then ( I -AtomicEval phi = (U -deltaInterpreter) . ((I -TermEval) * (SubTerms phi)) & |.(ar ((S -firstChar) . phi)).| = 2 ) by Th14, A2;
then ( I -AtomicEval phi = 1 iff (I -TermEval) * (SubTerms phi) in (U -deltaInterpreter) " {1} ) by FOMODEL0:25;
then A4: ( I -AtomicEval phi = 1 iff (I -TermEval) * (SubTerms phi) in { <*u,u*> where u is Element of U : verum } ) by Th13;
reconsider pp = SubTerms phi as 2 -element FinSequence of AllTermsOf S by FINSEQ_1:def 11, A3, A2;
reconsider q = (I -TermEval) * pp as FinSequence of U ;
reconsider qq = q as Element of 2 -tuples_on U by FOMODEL0:16;
qq in 2 -tuples_on U ;
then consider u1, u2 being Element of U such that
A5: qq = <*u1,u2*> by A1;
1 <= 2 ;
then ( 1 <= 1 & 1 <= len q & 1 <= 2 & 2 <= len q ) by CARD_1:def 7;
then ( 1 in Seg (len q) & 2 in Seg (len q) ) ;
then ( 1 in dom q & 2 in dom q ) by FINSEQ_1:def 3;
then A7: ( q . 1 = (I -TermEval) . ((SubTerms phi) . 1) & q . 2 = (I -TermEval) . ((SubTerms phi) . 2) ) by FUNCT_1:12;
( q in { <*u,u*> where u is Element of U : verum } implies (I -TermEval) . ((SubTerms phi) . 1) = (I -TermEval) . ((SubTerms phi) . 2) )

proof

assume q in { <*u,u*> where u is Element of U : verum } ; :: thesis: (I -TermEval) . ((SubTerms phi) . 1) = (I -TermEval) . ((SubTerms phi) . 2)
then consider u being Element of U such that
A8: <*u,u*> = q ;
( q . 1 = u & q . 2 = u ) by A8;
hence (I -TermEval) . ((SubTerms phi) . 1) = (I -TermEval) . ((SubTerms phi) . 2) by A7; :: thesis: verum

end;

hence ( I -AtomicEval phi = 1 iff (I -TermEval) . ((SubTerms phi) . 1) = (I -TermEval) . ((SubTerms phi) . 2) ) by A4, A7, A5; :: thesis: verum