set II = U -InterpretersOf S;

set AF = AtomicFormulasOf S;

deffunc H_{1}( Element of U -InterpretersOf S, Element of AtomicFormulasOf S) -> Element of BOOLEAN = $1 -AtomicEval $2;

consider f being Function of [:(U -InterpretersOf S),(AtomicFormulasOf S):],BOOLEAN such that

A1: for I being Element of U -InterpretersOf S

for phi being Element of AtomicFormulasOf S holds f . (I,phi) = H_{1}(I,phi)
from BINOP_1:sch 4();

take f ; :: thesis: for I being Element of U -InterpretersOf S

for phi being Element of AtomicFormulasOf S holds f . (I,phi) = I -AtomicEval phi

thus for I being Element of U -InterpretersOf S

for phi being Element of AtomicFormulasOf S holds f . (I,phi) = I -AtomicEval phi by A1; :: thesis: verum

set AF = AtomicFormulasOf S;

deffunc H

consider f being Function of [:(U -InterpretersOf S),(AtomicFormulasOf S):],BOOLEAN such that

A1: for I being Element of U -InterpretersOf S

for phi being Element of AtomicFormulasOf S holds f . (I,phi) = H

take f ; :: thesis: for I being Element of U -InterpretersOf S

for phi being Element of AtomicFormulasOf S holds f . (I,phi) = I -AtomicEval phi

thus for I being Element of U -InterpretersOf S

for phi being Element of AtomicFormulasOf S holds f . (I,phi) = I -AtomicEval phi by A1; :: thesis: verum