let m be Nat; :: thesis: for S being Language
for U being non empty set holds dom (NorIterator ((S,U) -TruthEval m)) = [:(U -InterpretersOf S),(m -NorFormulasOf S):]
let S be Language; :: thesis: for U being non empty set holds dom (NorIterator ((S,U) -TruthEval m)) = [:(U -InterpretersOf S),(m -NorFormulasOf S):]
let U be non empty set ; :: thesis: dom (NorIterator ((S,U) -TruthEval m)) = [:(U -InterpretersOf S),(m -NorFormulasOf S):]
set mm = m;
set II = U -InterpretersOf S;
set SS = AllSymbolsOf S;
set N = TheNorSymbOf S;
set Fm = (S,U) -TruthEval m;
set Phim = S -formulasOfMaxDepth m;
set IT = NorIterator ((S,U) -TruthEval m);
deffunc H₁( FinSequence, FinSequence) -> set = (<*(TheNorSymbOf S)*> ^ $1) ^ $2;
defpred S₁[] means verum;
set A = { H₁(phi1,phi2) where phi1, phi2 is Element of S -formulasOfMaxDepth m : S₁[] } ;
set LH = dom (NorIterator ((S,U) -TruthEval m));
set RH = [:(U -InterpretersOf S), { H₁(phi1,phi2) where phi1, phi2 is Element of S -formulasOfMaxDepth m : S₁[] } :];
(S,U) -TruthEval m is Element of Funcs ([:(U -InterpretersOf S),(S -formulasOfMaxDepth m):],BOOLEAN) by Lm32;
then reconsider Fmm = (S,U) -TruthEval m as Function of [:(U -InterpretersOf S),(S -formulasOfMaxDepth m):],BOOLEAN ;
B1: dom Fmm = [:(U -InterpretersOf S),(S -formulasOfMaxDepth m):] by FUNCT_2:def 1;
reconsider ITT = NorIterator ((S,U) -TruthEval m) as PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN ;
B2: [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):] = { [x,y] where x is Element of U -InterpretersOf S, y is Element of ((AllSymbolsOf S) *) \ {{}} : verum } by DOMAIN_1:19;

now

let z be set ; :: thesis: ( z in dom (NorIterator ((S,U) -TruthEval m)) implies z in [:(U -InterpretersOf S), { H₁(phi1,phi2) where phi1, phi2 is Element of S -formulasOfMaxDepth m : S₁[] } :] )
assume D0: z in dom (NorIterator ((S,U) -TruthEval m)) ; :: thesis: z in [:(U -InterpretersOf S), { H₁(phi1,phi2) where phi1, phi2 is Element of S -formulasOfMaxDepth m : S₁[] } :]
then z in [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):] ;
then consider x being Element of U -InterpretersOf S, y being Element of ((AllSymbolsOf S) *) \ {{}} such that
D1: z = [x,y] by B2;
consider phi1, phi2 being Element of ((AllSymbolsOf S) *) \ {{}} such that
D2: ( y = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 & [x,phi1] in dom ((S,U) -TruthEval m) & [x,phi2] in dom ((S,U) -TruthEval m) ) by DefNorIter, D0, D1;
reconsider phi11 = phi1, phi22 = phi2 as Element of S -formulasOfMaxDepth m by D2, B1, ZFMISC_1:87;
set yy = H₁(phi11,phi22);
( x in U -InterpretersOf S & H₁(phi11,phi22) in { H₁(phi1,phi2) where phi1, phi2 is Element of S -formulasOfMaxDepth m : S₁[] } & z = [x,H₁(phi11,phi22)] ) by D1, D2;
hence z in [:(U -InterpretersOf S), { H₁(phi1,phi2) where phi1, phi2 is Element of S -formulasOfMaxDepth m : S₁[] } :] by ZFMISC_1:def 2; :: thesis: verum

end;

then B5: dom (NorIterator ((S,U) -TruthEval m)) c= [:(U -InterpretersOf S), { H₁(phi1,phi2) where phi1, phi2 is Element of S -formulasOfMaxDepth m : S₁[] } :] by TARSKI:def 3;

now

let z be set ; :: thesis: ( z in [:(U -InterpretersOf S), { H₁(phi1,phi2) where phi1, phi2 is Element of S -formulasOfMaxDepth m : S₁[] } :] implies z in dom (NorIterator ((S,U) -TruthEval m)) )
assume z in [:(U -InterpretersOf S), { H₁(phi1,phi2) where phi1, phi2 is Element of S -formulasOfMaxDepth m : S₁[] } :] ; :: thesis: z in dom (NorIterator ((S,U) -TruthEval m))
then consider xx, yy being set such that
D0: ( xx in U -InterpretersOf S & yy in { H₁(phi1,phi2) where phi1, phi2 is Element of S -formulasOfMaxDepth m : S₁[] } & z = [xx,yy] ) by ZFMISC_1:def 2;
reconsider x = xx as Element of U -InterpretersOf S by D0;
consider phi1, phi2 being Element of S -formulasOfMaxDepth m such that
D1: yy = H₁(phi1,phi2) by D0;
reconsider phi11 = phi1, phi22 = phi2 as string of S ;
(<*(TheNorSymbOf S)*> ^ phi11) ^ phi22 is string of S ;
then reconsider y = yy as string of S by D1;
( [x,phi1] in dom Fmm & [x,phi2] in dom Fmm ) by B1;
then [x,y] in dom (NorIterator ((S,U) -TruthEval m)) by D1, DefNorIter;
hence z in dom (NorIterator ((S,U) -TruthEval m)) by D0; :: thesis: verum

end;

then [:(U -InterpretersOf S), { H₁(phi1,phi2) where phi1, phi2 is Element of S -formulasOfMaxDepth m : S₁[] } :] c= dom (NorIterator ((S,U) -TruthEval m)) by TARSKI:def 3;
hence dom (NorIterator ((S,U) -TruthEval m)) = [:(U -InterpretersOf S),(m -NorFormulasOf S):] by B5, XBOOLE_0:def 10; :: thesis: verum