let S be Language; :: thesis: for U being non empty set
for phi1, phi2 being wff string of S
for I being Element of U -InterpretersOf S holds
( I -TruthEval ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) = TRUE iff ( I -TruthEval phi1 = FALSE & I -TruthEval phi2 = FALSE ) )
let U be non empty set ; :: thesis: for phi1, phi2 being wff string of S
for I being Element of U -InterpretersOf S holds
( I -TruthEval ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) = TRUE iff ( I -TruthEval phi1 = FALSE & I -TruthEval phi2 = FALSE ) )
let phi1, phi2 be wff string of S; :: thesis: for I being Element of U -InterpretersOf S holds
( I -TruthEval ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) = TRUE iff ( I -TruthEval phi1 = FALSE & I -TruthEval phi2 = FALSE ) )
let I be Element of U -InterpretersOf S; :: thesis: ( I -TruthEval ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) = TRUE iff ( I -TruthEval phi1 = FALSE & I -TruthEval phi2 = FALSE ) )
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 ;
set m = max ((Depth phi1),(Depth phi2));
set M = (max ((Depth phi1),(Depth phi2))) + 1;
reconsider d1 = (max ((Depth phi1),(Depth phi2))) - (Depth phi1), d2 = (max ((Depth phi1),(Depth phi2))) - (Depth phi2) as Nat ;
( phi1 is (Depth phi1) + (0 * d1) -wff & phi2 is (Depth phi2) + (0 * d2) -wff ) by DefDepth;
then ( phi1 is (Depth phi1) + d1 -wff & phi2 is (Depth phi2) + d2 -wff ) ;
then reconsider phi11 = phi1, phi22 = phi2 as max ((Depth phi1),(Depth phi2)) -wff string of S ;
reconsider phi = (<*(TheNorSymbOf S)*> ^ phi11) ^ phi22 as (max ((Depth phi1),(Depth phi2))) + 1 -wff string of S ;
reconsider mm = max ((Depth phi1),(Depth phi2)), MM = (max ((Depth phi1),(Depth phi2))) + 1 as Element of NAT by ORDINAL1:def 12;
set Phim = S -formulasOfMaxDepth (max ((Depth phi1),(Depth phi2)));
set PhiM = S -formulasOfMaxDepth ((max ((Depth phi1),(Depth phi2))) + 1);
set FM = (S,U) -TruthEval ((max ((Depth phi1),(Depth phi2))) + 1);
set Fm = (S,U) -TruthEval (max ((Depth phi1),(Depth phi2)));
set mNF = (max ((Depth phi1),(Depth phi2))) -NorFormulasOf S;
B4: I -TruthEval phi1 = ((I,(max ((Depth phi1),(Depth phi2)))) -TruthEval) . phi11 by DefTruth4
.= ((S,U) -TruthEval (max ((Depth phi1),(Depth phi2)))) . (I,phi1) by Lm41 ;
Z1: I -TruthEval phi22 = ((I,(max ((Depth phi1),(Depth phi2)))) -TruthEval) . phi22 by DefTruth4
.= ((S,U) -TruthEval (max ((Depth phi1),(Depth phi2)))) . (I,phi2) by Lm41 ;
reconsider phi111 = phi11, phi222 = phi22 as Element of S -formulasOfMaxDepth (max ((Depth phi1),(Depth phi2))) by DefWff1;
phi = (<*(TheNorSymbOf S)*> ^ phi111) ^ phi222 ;
then phi in (max ((Depth phi1),(Depth phi2))) -NorFormulasOf S ;
then [I,phi] in [:(U -InterpretersOf S),((max ((Depth phi1),(Depth phi2))) -NorFormulasOf S):] by ZFMISC_1:87;
then B5: [I,phi] in dom (NorIterator ((S,U) -TruthEval (max ((Depth phi1),(Depth phi2))))) by Lm33;
B6: ((S,U) -TruthEval) . MM = ((ExIterator (((S,U) -TruthEval) . mm)) +* (NorIterator (((S,U) -TruthEval) . mm))) +* (((S,U) -TruthEval) . mm) by DefTruth1;
(S,U) -TruthEval (max ((Depth phi1),(Depth phi2))) is Element of Funcs ([:(U -InterpretersOf S),(S -formulasOfMaxDepth (max ((Depth phi1),(Depth phi2)))):],BOOLEAN) by Lm32;
then reconsider Fmm = (S,U) -TruthEval (max ((Depth phi1),(Depth phi2))) as Function of [:(U -InterpretersOf S),(S -formulasOfMaxDepth (max ((Depth phi1),(Depth phi2)))):],BOOLEAN ;
B7: not [I,phi] in dom (((S,U) -TruthEval) . mm)

proof

Z3: not phi in S -formulasOfMaxDepth (max ((Depth phi1),(Depth phi2))) by DefWff1;
dom (((S,U) -TruthEval) . mm) = dom Fmm by DefTruth2
.= [:(U -InterpretersOf S),(S -formulasOfMaxDepth (max ((Depth phi1),(Depth phi2)))):] by FUNCT_2:def 1 ;
hence not [I,phi] in dom (((S,U) -TruthEval) . mm) by Z3, ZFMISC_1:87; :: thesis: verum

end;

Z4: dom Fmm = [:(U -InterpretersOf S),(S -formulasOfMaxDepth (max ((Depth phi1),(Depth phi2)))):] by FUNCT_2:def 1;
I -TruthEval phi = ((I,((max ((Depth phi1),(Depth phi2))) + 1)) -TruthEval) . phi by DefTruth4
.= ((S,U) -TruthEval ((max ((Depth phi1),(Depth phi2))) + 1)) . [I,phi] by Lm41
.= (((S,U) -TruthEval) . MM) . [I,phi] by DefTruth2
.= ((ExIterator (((S,U) -TruthEval) . mm)) +* (NorIterator (((S,U) -TruthEval) . mm))) . [I,phi] by B6, B7, FUNCT_4:11
.= ((ExIterator (((S,U) -TruthEval) . mm)) +* (NorIterator ((S,U) -TruthEval (max ((Depth phi1),(Depth phi2)))))) . [I,phi] by DefTruth2
.= H₂((S,U) -TruthEval (max ((Depth phi1),(Depth phi2)))) . (I,phi) by B5, FUNCT_4:13
.= ((S,U) -TruthEval (max ((Depth phi1),(Depth phi2)))) -NorFunctor (I,phi) by B5, DefNorIter ;
hence ( I -TruthEval ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) = TRUE iff ( I -TruthEval phi1 = FALSE & I -TruthEval phi2 = FALSE ) ) by Z4, Lm38, Z1, B4; :: thesis: verum