set II = U -InterpretersOf S;
set AF = AtomicFormulasOf S;
set B = BOOLEAN ;
let IT1, IT2 be Function of [:(U -InterpretersOf S),(AtomicFormulasOf S):],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 H₁( 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) = H₁(I,phi) and
A3: for I being Element of U -InterpretersOf S
for phi being Element of AtomicFormulasOf S holds IT2 . (I,phi) = H₁(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) = H₁(a,b) by A2
.= IT2 . (a,b) by A3 ; :: thesis: verum

end;

hence IT1 = IT2 ; :: thesis: verum