set II = U -InterpretersOf S;
set AF = AtomicFormulasOf S;
set B = BOOLEAN ;
let IT1, IT2 be Function of [:(),():],BOOLEAN; :: thesis: ( ( for I being Element of U -InterpretersOf S
for phi being Element of AtomicFormulasOf S holds IT1 . (I,phi) = I -AtomicEval phi ) & ( for I being Element of U -InterpretersOf S
for phi being Element of AtomicFormulasOf S holds IT2 . (I,phi) = I -AtomicEval phi ) implies IT1 = IT2 )

deffunc H1( Element of U -InterpretersOf S, Element of AtomicFormulasOf S) -> Element of BOOLEAN = \$1 -AtomicEval \$2;
assume that
A2: for I being Element of U -InterpretersOf S
for phi being Element of AtomicFormulasOf S holds IT1 . (I,phi) = H1(I,phi) and
A3: for I being Element of U -InterpretersOf S
for phi being Element of AtomicFormulasOf S holds IT2 . (I,phi) = H1(I,phi) ; :: thesis: IT1 = IT2
now :: thesis: for a being Element of U -InterpretersOf S
for b being Element of AtomicFormulasOf S holds IT1 . (a,b) = IT2 . (a,b)
let a be Element of U -InterpretersOf S; :: thesis: for b being Element of AtomicFormulasOf S holds IT1 . (a,b) = IT2 . (a,b)
let b be Element of AtomicFormulasOf S; :: thesis: IT1 . (a,b) = IT2 . (a,b)
thus IT1 . (a,b) = H1(a,b) by A2
.= IT2 . (a,b) by A3 ; :: thesis: verum
end;
hence IT1 = IT2 ; :: thesis: verum