let m be Nat; :: thesis: for S being Language holds S -formulasOfMaxDepth (m + 1) = (() \/ ()) \/ ()
let S be Language; :: thesis: S -formulasOfMaxDepth (m + 1) = (() \/ ()) \/ ()
set U = the non empty set ;
set n = m + 1;
set II = the non empty set -InterpretersOf S;
set SS = AllSymbolsOf S;
set N = TheNorSymbOf S;
set I = the Element of the non empty set -InterpretersOf S;
reconsider mm = m, nn = m + 1 as Element of NAT by ORDINAL1:def 12;
set F = (S, the non empty set ) -TruthEval ;
set Fn = ((S, the non empty set ) -TruthEval) . nn;
set Fc = curry (((S, the non empty set ) -TruthEval) . nn);
set Dm = S -formulasOfMaxDepth m;
set Dn = S -formulasOfMaxDepth (m + 1);
((S, the non empty set ) -TruthEval) . mm is Element of PFuncs ([:( the non empty set -InterpretersOf S),((() *) \ ):],BOOLEAN) ;
then reconsider Fm = ((S, the non empty set ) -TruthEval) . mm as PartFunc of [:( the non empty set -InterpretersOf S),((() *) \ ):],BOOLEAN ;
A1: ( (S, the non empty set ) -TruthEval (m + 1) = ((S, the non empty set ) -TruthEval) . nn & (S, the non empty set ) -TruthEval m = Fm ) by Def20;
reconsider Fcc = curry (((S, the non empty set ) -TruthEval) . nn) as Function of ( the non empty set -InterpretersOf S),(Funcs ((S -formulasOfMaxDepth (m + 1)),BOOLEAN)) by ;
reconsider fn = Fcc . the Element of the non empty set -InterpretersOf S as Function of (S -formulasOfMaxDepth (m + 1)),BOOLEAN ;
Fm is Element of Funcs ([:( the non empty set -InterpretersOf S),():],BOOLEAN) by Th8;
then reconsider Fmm = Fm as Function of [:( the non empty set -InterpretersOf S),():],BOOLEAN ;
( dom fn = S -formulasOfMaxDepth (m + 1) & dom Fcc = the non empty set -InterpretersOf S ) by FUNCT_2:def 1;
then A2: S -formulasOfMaxDepth (m + 1) = proj2 ((dom (((S, the non empty set ) -TruthEval) . nn)) /\ [:{ the Element of the non empty set -InterpretersOf S},(proj2 (dom (((S, the non empty set ) -TruthEval) . nn))):]) by FUNCT_5:31;
A3: ((S, the non empty set ) -TruthEval) . nn = ((ExIterator (((S, the non empty set ) -TruthEval) . mm)) +* (NorIterator (((S, the non empty set ) -TruthEval) . mm))) +* Fm by Def19;
reconsider Em = ExIterator (((S, the non empty set ) -TruthEval) . mm) as PartFunc of [:( the non empty set -InterpretersOf S),((() *) \ ):],BOOLEAN ;
reconsider dEm = dom Em as Relation of ( the non empty set -InterpretersOf S),((() *) \ ) ;
reconsider dNm = dom (NorIterator (((S, the non empty set ) -TruthEval) . mm)), dFm = dom Fm as Relation of ( the non empty set -InterpretersOf S),((() *) \ ) ;
A4: dFm = dom Fmm
.= [:( the non empty set -InterpretersOf S),():] by FUNCT_2:def 1 ;
A5: dom (((S, the non empty set ) -TruthEval) . nn) = (dom ((ExIterator (((S, the non empty set ) -TruthEval) . mm)) +* (NorIterator (((S, the non empty set ) -TruthEval) . mm)))) \/ (dom Fm) by
.= (dEm \/ dNm) \/ dFm by FUNCT_4:def 1 ;
set RNNN = m -NorFormulasOf S;
set REEE = m -ExFormulasOf S;
(S, the non empty set ) -TruthEval m = Fm by Def20;
then ( dNm = [:( the non empty set -InterpretersOf S),():] & dEm = [:( the non empty set -InterpretersOf S),():] ) by ;
then A6: (dEm \/ dNm) \/ dFm = [:( the non empty set -InterpretersOf S),(() \/ ()):] \/ [:( the non empty set -InterpretersOf S),():] by
.= [:( the non empty set -InterpretersOf S),((() \/ ()) \/ ()):] by ZFMISC_1:97 ;
reconsider sub = [:{ the Element of the non empty set -InterpretersOf S},((() \/ ()) \/ ()):] as Subset of [:( the non empty set -InterpretersOf S),((() \/ ()) \/ ()):] by ZFMISC_1:96;
S -formulasOfMaxDepth (m + 1) = rng ([:( the non empty set -InterpretersOf S),((() \/ ()) \/ ()):] /\ sub) by A6, A2, A5
.= (() \/ ()) \/ () ;
hence S -formulasOfMaxDepth (m + 1) = (() \/ ()) \/ () ; :: thesis: verum