let S be Language; :: thesis:
let U be non empty set ; :: thesis:
let phi1, phi2 be wff string of S; :: thesis:
let I be Element of U -InterpretersOf S; :: thesis:
set Nor = TheNorSymbOf S;
set II = U -InterpretersOf S;
set SS = AllSymbolsOf S;
set B = BOOLEAN ;
set D = PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN);
set m1 = Depth phi1;
set m2 = Depth phi2;
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 m = max ((Depth phi1),(Depth phi2)) as Nat by TARSKI:1;
set M = m + 1;
reconsider d1 = m - (Depth phi1), d2 = m - (Depth phi2) as Nat ;
( phi1 is (Depth phi1) + (0 * d1) -wff & phi2 is (Depth phi2) + (0 * d2) -wff ) by Def30;
then ( phi1 is (Depth phi1) + d1 -wff & phi2 is (Depth phi2) + d2 -wff ) ;
then reconsider phi11 = phi1, phi22 = phi2 as m -wff string of S ;
reconsider phi = (<*(TheNorSymbOf S)*> ^ phi11) ^ phi22 as m + 1 -wff string of S ;
reconsider mm = m, MM = m + 1 as Element of NAT by ORDINAL1:def 12;
set Phim = S -formulasOfMaxDepth m;
set PhiM = S -formulasOfMaxDepth (m + 1);
set FM = (S,U) -TruthEval (m + 1);
set Fm = (S,U) -TruthEval m;
set mNF = m -NorFormulasOf S;
A1: I -TruthEval phi1 = ((I,m) -TruthEval) . phi11 by Def25
.= ((S,U) -TruthEval m) . (I,phi1) by Lm33 ;
A2: I -TruthEval phi22 = ((I,m) -TruthEval) . phi22 by Def25
.= ((S,U) -TruthEval m) . (I,phi2) by Lm33 ;
reconsider phi111 = phi11, phi222 = phi22 as Element of S -formulasOfMaxDepth m by Def23;
phi = (<*(TheNorSymbOf S)*> ^ phi111) ^ phi222 ;
then phi in m -NorFormulasOf S ;
then [I,phi] in [:(U -InterpretersOf S),(m -NorFormulasOf S):] by ZFMISC_1:87;
then A3: [I,phi] in dom (NorIterator ((S,U) -TruthEval m)) by Lm18;
A4: ((S,U) -TruthEval) . MM = ((ExIterator (((S,U) -TruthEval) . mm)) +* (NorIterator (((S,U) -TruthEval) . mm))) +* (((S,U) -TruthEval) . mm) by Def19;
(S,U) -TruthEval m is Element of Funcs ([:(U -InterpretersOf S),(S -formulasOfMaxDepth m):],BOOLEAN) by Th8;
then reconsider Fmm = (S,U) -TruthEval m as Function of [:(U -InterpretersOf S),(S -formulasOfMaxDepth m):],BOOLEAN ;
A5: not [I,phi] in dom (((S,U) -TruthEval) . mm)

proof

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

end;

A7: dom Fmm = [:(U -InterpretersOf S),(S -formulasOfMaxDepth m):] by FUNCT_2:def 1;
I -TruthEval phi = ((I,(m + 1)) -TruthEval) . phi by Def25
.= ((S,U) -TruthEval (m + 1)) . [I,phi] by Lm33
.= (((S,U) -TruthEval) . MM) . [I,phi] by Def20
.= ((ExIterator (((S,U) -TruthEval) . mm)) +* (NorIterator (((S,U) -TruthEval) . mm))) . [I,phi] by A4, A5, FUNCT_4:11
.= ((ExIterator (((S,U) -TruthEval) . mm)) +* (NorIterator ((S,U) -TruthEval m))) . [I,phi] by Def20
.= H₂((S,U) -TruthEval m) . (I,phi) by FUNCT_4:13, A3
.= ((S,U) -TruthEval m) -NorFunctor (I,phi) by A3, Def18 ;
hence ( I -TruthEval ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) = TRUE iff ( I -TruthEval phi1 = FALSE & I -TruthEval phi2 = FALSE ) ) by A7, Lm36, A2, A1; :: thesis: