let S be Language; :: thesis: for U being non empty set
for l being literal Element of S
for phi being wff string of S
for I being Element of U -InterpretersOf S holds
( I -TruthEval (<*l*> ^ phi) = TRUE iff ex u being Element of U st ((l,u) ReassignIn I) -TruthEval phi = 1 )
let U be non empty set ; :: thesis: for l being literal Element of S
for phi being wff string of S
for I being Element of U -InterpretersOf S holds
( I -TruthEval (<*l*> ^ phi) = TRUE iff ex u being Element of U st ((l,u) ReassignIn I) -TruthEval phi = 1 )
let l be literal Element of S; :: thesis: for phi being wff string of S
for I being Element of U -InterpretersOf S holds
( I -TruthEval (<*l*> ^ phi) = TRUE iff ex u being Element of U st ((l,u) ReassignIn I) -TruthEval phi = 1 )
let phi be wff string of S; :: thesis: for I being Element of U -InterpretersOf S holds
( I -TruthEval (<*l*> ^ phi) = TRUE iff ex u being Element of U st ((l,u) ReassignIn I) -TruthEval phi = 1 )
let I be Element of U -InterpretersOf S; :: thesis: ( I -TruthEval (<*l*> ^ phi) = TRUE iff ex u being Element of U st ((l,u) ReassignIn I) -TruthEval phi = 1 )
set Nor = TheNorSymbOf S;
set II = U -InterpretersOf S;
set SS = AllSymbolsOf S;
set D = PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN);
set m = Depth phi;
set M = (Depth phi) + 1;
set L = LettersOf S;
reconsider phii = phi as Depth phi -wff string of S by Def30;
reconsider psi = <*l*> ^ phi as (Depth phi) + 1 -wff string of S ;
deffunc H₁( Element of PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN)) -> PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN = ExIterator $1;
deffunc H₂( Element of PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN)) -> PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN = NorIterator $1;
set F = (S,U) -TruthEval ;
reconsider mm = Depth phi, MM = (Depth phi) + 1 as Element of NAT by ORDINAL1:def 12;
set Phim = S -formulasOfMaxDepth (Depth phi);
set PhiM = S -formulasOfMaxDepth ((Depth phi) + 1);
reconsider phiii = phii as Element of S -formulasOfMaxDepth (Depth phi) by Def23;
reconsider ll = l as Element of LettersOf S by FOMODEL1:def 14;
set FM = (S,U) -TruthEval ((Depth phi) + 1);
set Fm = (S,U) -TruthEval (Depth phi);
set mNF = (Depth phi) -NorFormulasOf S;
set mEF = (Depth phi) -ExFormulasOf S;
psi = <*ll*> ^ phiii ;
then ( psi in (Depth phi) -ExFormulasOf S & not psi in (Depth phi) -NorFormulasOf S ) ;
then ( [I,psi] in [:(U -InterpretersOf S),((Depth phi) -ExFormulasOf S):] & not [I,psi] in [:(U -InterpretersOf S),((Depth phi) -NorFormulasOf S):] ) by ZFMISC_1:87;
then A1: ( [I,psi] in dom (ExIterator ((S,U) -TruthEval (Depth phi))) & not [I,psi] in dom (NorIterator ((S,U) -TruthEval (Depth phi))) ) by Lm18, Lm19;
A2: ((S,U) -TruthEval) . MM = ((ExIterator (((S,U) -TruthEval) . mm)) +* (NorIterator (((S,U) -TruthEval) . mm))) +* (((S,U) -TruthEval) . mm) by Def19;
(S,U) -TruthEval (Depth phi) is Element of Funcs ([:(U -InterpretersOf S),(S -formulasOfMaxDepth (Depth phi)):],BOOLEAN) by Th8;
then reconsider Fmm = (S,U) -TruthEval (Depth phi) as Function of [:(U -InterpretersOf S),(S -formulasOfMaxDepth (Depth phi)):],BOOLEAN ;
A3: not [I,psi] in dom (((S,U) -TruthEval) . mm)

proof

A4: not psi in S -formulasOfMaxDepth (Depth phi) by Def23;
dom (((S,U) -TruthEval) . mm) = dom Fmm by Def20
.= [:(U -InterpretersOf S),(S -formulasOfMaxDepth (Depth phi)):] by FUNCT_2:def 1 ;
hence not [I,psi] in dom (((S,U) -TruthEval) . mm) by A4, ZFMISC_1:87; :: thesis: verum

end;

A5: dom Fmm = [:(U -InterpretersOf S),(S -formulasOfMaxDepth (Depth phi)):] by FUNCT_2:def 1;
A6: I -TruthEval psi = ((I,((Depth phi) + 1)) -TruthEval) . psi by Def25
.= ((S,U) -TruthEval ((Depth phi) + 1)) . [I,psi] by Lm33
.= (((S,U) -TruthEval) . MM) . [I,psi] by Def20
.= ((ExIterator (((S,U) -TruthEval) . mm)) +* (NorIterator (((S,U) -TruthEval) . mm))) . [I,psi] by A2, A3, FUNCT_4:11
.= ((ExIterator (((S,U) -TruthEval) . mm)) +* (NorIterator ((S,U) -TruthEval (Depth phi)))) . [I,psi] by Def20
.= (ExIterator (((S,U) -TruthEval) . mm)) . [I,psi] by FUNCT_4:11, A1
.= H₁((S,U) -TruthEval (Depth phi)) . (I,psi) by Def20
.= ((S,U) -TruthEval (Depth phi)) -ExFunctor (I,psi) by A1, Def16 ;
A7: ( ex u being Element of U st ((S,U) -TruthEval (Depth phi)) . (((l,u) ReassignIn I),phii) = TRUE implies ex u being Element of U st ((l,u) ReassignIn I) -TruthEval phii = TRUE )

proof

given u being Element of U such that A8: ((S,U) -TruthEval (Depth phi)) . (((l,u) ReassignIn I),phii) = TRUE ; :: thesis: ex u being Element of U st ((l,u) ReassignIn I) -TruthEval phii = TRUE
take u ; :: thesis: ((l,u) ReassignIn I) -TruthEval phii = TRUE
set J = (l,u) ReassignIn I;
((((l,u) ReassignIn I),(Depth phi)) -TruthEval) . phii = TRUE by A8, Lm33;
hence ((l,u) ReassignIn I) -TruthEval phii = TRUE by Def25; :: thesis: verum

end;

( ex u being Element of U st ((l,u) ReassignIn I) -TruthEval phii = TRUE implies ex u being Element of U st ((S,U) -TruthEval (Depth phi)) . (((l,u) ReassignIn I),phii) = TRUE )

proof

given u being Element of U such that A9: ((l,u) ReassignIn I) -TruthEval phii = TRUE ; :: thesis: ex u being Element of U st ((S,U) -TruthEval (Depth phi)) . (((l,u) ReassignIn I),phii) = TRUE
take u ; :: thesis: ((S,U) -TruthEval (Depth phi)) . (((l,u) ReassignIn I),phii) = TRUE
set J = (l,u) ReassignIn I;
((((l,u) ReassignIn I),(Depth phi)) -TruthEval) . phii = TRUE by A9, Def25;
hence ((S,U) -TruthEval (Depth phi)) . (((l,u) ReassignIn I),phii) = TRUE by Lm33; :: thesis: verum

end;

hence ( I -TruthEval (<*l*> ^ phi) = TRUE iff ex u being Element of U st ((l,u) ReassignIn I) -TruthEval phi = 1 ) by A6, A5, Lm34, A7; :: thesis: verum