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