let S be Language; 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 ; 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; 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; 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
; verum