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_{1}( 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_{1}(I,phi)
and

A3: for I being Element of U -InterpretersOf S

for phi being Element of AtomicFormulasOf S holds IT2 . (I,phi) = H_{1}(I,phi)
; :: thesis: IT1 = IT2

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

assume that

A2: for I being Element of U -InterpretersOf S

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

A3: for I being Element of U -InterpretersOf S

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

now :: thesis: for a being Element of U -InterpretersOf S

for b being Element of AtomicFormulasOf S holds IT1 . (a,b) = IT2 . (a,b)

hence
IT1 = IT2
; :: thesis: verumfor 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_{1}(a,b)
by A2

.= IT2 . (a,b) by A3 ; :: thesis: verum

end;let b be Element of AtomicFormulasOf S; :: thesis: IT1 . (a,b) = IT2 . (a,b)

thus IT1 . (a,b) = H

.= IT2 . (a,b) by A3 ; :: thesis: verum