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 ((<*()*> ^ 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 ((<*()*> ^ 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 ((<*()*> ^ phi1) ^ phi2) = TRUE iff ( I -TruthEval phi1 = FALSE & I -TruthEval phi2 = FALSE ) )

let I be Element of U -InterpretersOf S; :: thesis: ( I -TruthEval ((<*()*> ^ 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 ([:(),((() *) \ ):],BOOLEAN);
set m1 = Depth phi1;
set m2 = Depth phi2;
deffunc H1( Element of PFuncs ([:(),((() *) \ ):],BOOLEAN)) -> PartFunc of [:(),((() *) \ ):],BOOLEAN = ExIterator \$1;
deffunc H2( Element of PFuncs ([:(),((() *) \ ):],BOOLEAN)) -> PartFunc of [:(),((() *) \ ):],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 = (<*()*> ^ 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 = (<*()*> ^ phi111) ^ phi222 ;
then phi in m -NorFormulasOf S ;
then [I,phi] in [:(),():] 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 ([:(),():],BOOLEAN) by Th8;
then reconsider Fmm = (S,U) -TruthEval m as Function of [:(),():],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
.= [:(),():] by FUNCT_2:def 1 ;
hence not [I,phi] in dom (((S,U) -TruthEval) . mm) by ; :: thesis: verum
end;
A7: dom Fmm = [:(),():] 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
.= ((ExIterator (((S,U) -TruthEval) . mm)) +* (NorIterator ((S,U) -TruthEval m))) . [I,phi] by Def20
.= H2((S,U) -TruthEval m) . (I,phi) by
.= ((S,U) -TruthEval m) -NorFunctor (I,phi) by ;
hence ( I -TruthEval ((<*()*> ^ phi1) ^ phi2) = TRUE iff ( I -TruthEval phi1 = FALSE & I -TruthEval phi2 = FALSE ) ) by A7, Lm36, A2, A1; :: thesis: verum