set F = S -firstChar ;

set i = I -TermEval ;

set A = AllTermsOf S;

reconsider s = (S -firstChar) . phi as relational Element of S ;

set n = |.(ar s).|;

reconsider f = (I ===) . s as Interpreter of s,U ;

reconsider ff = f as Function of (|.(ar s).| -tuples_on U),BOOLEAN by Def2;

reconsider V = SubTerms phi as |.(ar s).| -element FinSequence of AllTermsOf S by FINSEQ_1:def 11;

reconsider iV = (I -TermEval) * V as |.(ar s).| -element FinSequence of U ;

len iV = |.(ar s).| by CARD_1:def 7;

then reconsider iVV = iV as Element of |.(ar s).| -tuples_on U by FINSEQ_2:133;

ff . iVV is Element of BOOLEAN ;

hence I -AtomicEval phi is Element of BOOLEAN ; :: thesis: verum

set i = I -TermEval ;

set A = AllTermsOf S;

reconsider s = (S -firstChar) . phi as relational Element of S ;

set n = |.(ar s).|;

reconsider f = (I ===) . s as Interpreter of s,U ;

reconsider ff = f as Function of (|.(ar s).| -tuples_on U),BOOLEAN by Def2;

reconsider V = SubTerms phi as |.(ar s).| -element FinSequence of AllTermsOf S by FINSEQ_1:def 11;

reconsider iV = (I -TermEval) * V as |.(ar s).| -element FinSequence of U ;

len iV = |.(ar s).| by CARD_1:def 7;

then reconsider iVV = iV as Element of |.(ar s).| -tuples_on U by FINSEQ_2:133;

ff . iVV is Element of BOOLEAN ;

hence I -AtomicEval phi is Element of BOOLEAN ; :: thesis: verum