let S be Language; :: thesis: for U being non empty set

for phi0 being 0wff string of S

for I being Element of U -InterpretersOf S holds I -TruthEval phi0 = I -AtomicEval phi0

let U be non empty set ; :: thesis: for phi0 being 0wff string of S

for I being Element of U -InterpretersOf S holds I -TruthEval phi0 = I -AtomicEval phi0

let phi0 be 0wff string of S; :: thesis: for I being Element of U -InterpretersOf S holds I -TruthEval phi0 = I -AtomicEval phi0

set II = U -InterpretersOf S;

let I be Element of U -InterpretersOf S; :: thesis: I -TruthEval phi0 = I -AtomicEval phi0

set LH = I -TruthEval phi0;

set RH = I -AtomicEval phi0;

set f = (S,U) -TruthEval 0;

set Phi0 = S -formulasOfMaxDepth 0;

set AF = AtomicFormulasOf S;

set SS = AllSymbolsOf S;

reconsider phi000 = phi0 as Element of S -formulasOfMaxDepth 0 by Def23;

reconsider phi00 = phi000 as Element of AtomicFormulasOf S by Lm16;

reconsider z = 0 as Element of NAT ;

(I,0) -TruthEval is Element of Funcs ((S -formulasOfMaxDepth 0),BOOLEAN) by Th24;

then reconsider g = (I,0) -TruthEval as Function of (S -formulasOfMaxDepth 0),BOOLEAN ;

set F = curry ((S,U) -TruthEval 0);

reconsider F = curry ((S,U) -TruthEval 0) as Function of (U -InterpretersOf S),(PFuncs ((((AllSymbolsOf S) *) \ {{}}),BOOLEAN)) by Lm11;

( dom F = U -InterpretersOf S & dom g = S -formulasOfMaxDepth 0 ) by FUNCT_2:def 1;

then ( I in dom F & g = F . I & phi000 in dom g ) ;

then A1: ( g . phi0 = ((S,U) -TruthEval 0) . (I,phi0) & [I,phi0] in dom ((S,U) -TruthEval 0) ) by FUNCT_5:31;

I -TruthEval phi0 = g . phi0 by Def25

.= (((S,U) -TruthEval) . z) . [I,phi0] by A1, Def20

.= (S -TruthEval U) . (I,phi00) by Def19

.= I -AtomicEval phi0 by Def14 ;

hence I -TruthEval phi0 = I -AtomicEval phi0 ; :: thesis: verum

for phi0 being 0wff string of S

for I being Element of U -InterpretersOf S holds I -TruthEval phi0 = I -AtomicEval phi0

let U be non empty set ; :: thesis: for phi0 being 0wff string of S

for I being Element of U -InterpretersOf S holds I -TruthEval phi0 = I -AtomicEval phi0

let phi0 be 0wff string of S; :: thesis: for I being Element of U -InterpretersOf S holds I -TruthEval phi0 = I -AtomicEval phi0

set II = U -InterpretersOf S;

let I be Element of U -InterpretersOf S; :: thesis: I -TruthEval phi0 = I -AtomicEval phi0

set LH = I -TruthEval phi0;

set RH = I -AtomicEval phi0;

set f = (S,U) -TruthEval 0;

set Phi0 = S -formulasOfMaxDepth 0;

set AF = AtomicFormulasOf S;

set SS = AllSymbolsOf S;

reconsider phi000 = phi0 as Element of S -formulasOfMaxDepth 0 by Def23;

reconsider phi00 = phi000 as Element of AtomicFormulasOf S by Lm16;

reconsider z = 0 as Element of NAT ;

(I,0) -TruthEval is Element of Funcs ((S -formulasOfMaxDepth 0),BOOLEAN) by Th24;

then reconsider g = (I,0) -TruthEval as Function of (S -formulasOfMaxDepth 0),BOOLEAN ;

set F = curry ((S,U) -TruthEval 0);

reconsider F = curry ((S,U) -TruthEval 0) as Function of (U -InterpretersOf S),(PFuncs ((((AllSymbolsOf S) *) \ {{}}),BOOLEAN)) by Lm11;

( dom F = U -InterpretersOf S & dom g = S -formulasOfMaxDepth 0 ) by FUNCT_2:def 1;

then ( I in dom F & g = F . I & phi000 in dom g ) ;

then A1: ( g . phi0 = ((S,U) -TruthEval 0) . (I,phi0) & [I,phi0] in dom ((S,U) -TruthEval 0) ) by FUNCT_5:31;

I -TruthEval phi0 = g . phi0 by Def25

.= (((S,U) -TruthEval) . z) . [I,phi0] by A1, Def20

.= (S -TruthEval U) . (I,phi00) by Def19

.= I -AtomicEval phi0 by Def14 ;

hence I -TruthEval phi0 = I -AtomicEval phi0 ; :: thesis: verum