let m be Nat; :: thesis: for S being Language
for U being non empty set holds dom (NorIterator ((S,U) -TruthEval m)) = [:(),():]

let S be Language; :: thesis: for U being non empty set holds dom (NorIterator ((S,U) -TruthEval m)) = [:(),():]
let U be non empty set ; :: thesis: dom (NorIterator ((S,U) -TruthEval m)) = [:(),():]
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 H1( FinSequence, FinSequence) -> set = (<*()*> ^ \$1) ^ \$2;
defpred S1[] means verum;
set A = { H1(phi1,phi2) where phi1, phi2 is Element of S -formulasOfMaxDepth m : S1[] } ;
set LH = dom (NorIterator ((S,U) -TruthEval m));
set RH = [:(), { H1(phi1,phi2) where phi1, phi2 is Element of S -formulasOfMaxDepth m : S1[] } :];
(S,U) -TruthEval m is Element of Funcs ([:(),():],BOOLEAN) by Th8;
then reconsider Fmm = (S,U) -TruthEval m as Function of [:(),():],BOOLEAN ;
A1: dom Fmm = [:(),():] by FUNCT_2:def 1;
reconsider ITT = NorIterator ((S,U) -TruthEval m) as PartFunc of [:(),((() *) \ ):],BOOLEAN ;
A2: [:(),((() *) \ ):] = { [x,y] where x is Element of U -InterpretersOf S, y is Element of (() *) \ : verum } by DOMAIN_1:19;
now :: thesis: for z being object st z in dom (NorIterator ((S,U) -TruthEval m)) holds
z in [:(), { H1(phi1,phi2) where phi1, phi2 is Element of S -formulasOfMaxDepth m : S1[] } :]
let z be object ; :: thesis: ( z in dom (NorIterator ((S,U) -TruthEval m)) implies z in [:(), { H1(phi1,phi2) where phi1, phi2 is Element of S -formulasOfMaxDepth m : S1[] } :] )
assume A3: z in dom (NorIterator ((S,U) -TruthEval m)) ; :: thesis: z in [:(), { H1(phi1,phi2) where phi1, phi2 is Element of S -formulasOfMaxDepth m : S1[] } :]
then z in [:(),((() *) \ ):] ;
then consider x being Element of U -InterpretersOf S, y being Element of (() *) \ such that
A4: z = [x,y] by A2;
consider phi1, phi2 being Element of (() *) \ such that
A5: ( y = (<*()*> ^ phi1) ^ phi2 & [x,phi1] in dom ((S,U) -TruthEval m) & [x,phi2] in dom ((S,U) -TruthEval m) ) by ;
reconsider phi11 = phi1, phi22 = phi2 as Element of S -formulasOfMaxDepth m by ;
set yy = H1(phi11,phi22);
( x in U -InterpretersOf S & H1(phi11,phi22) in { H1(phi1,phi2) where phi1, phi2 is Element of S -formulasOfMaxDepth m : S1[] } & z = [x,H1(phi11,phi22)] ) by A4, A5;
hence z in [:(), { H1(phi1,phi2) where phi1, phi2 is Element of S -formulasOfMaxDepth m : S1[] } :] by ZFMISC_1:def 2; :: thesis: verum
end;
then A6: dom (NorIterator ((S,U) -TruthEval m)) c= [:(), { H1(phi1,phi2) where phi1, phi2 is Element of S -formulasOfMaxDepth m : S1[] } :] ;
now :: thesis: for z being object st z in [:(), { H1(phi1,phi2) where phi1, phi2 is Element of S -formulasOfMaxDepth m : S1[] } :] holds
z in dom (NorIterator ((S,U) -TruthEval m))
let z be object ; :: thesis: ( z in [:(), { H1(phi1,phi2) where phi1, phi2 is Element of S -formulasOfMaxDepth m : S1[] } :] implies z in dom (NorIterator ((S,U) -TruthEval m)) )
assume z in [:(), { H1(phi1,phi2) where phi1, phi2 is Element of S -formulasOfMaxDepth m : S1[] } :] ; :: thesis: z in dom (NorIterator ((S,U) -TruthEval m))
then consider xx, yy being object such that
A7: ( xx in U -InterpretersOf S & yy in { H1(phi1,phi2) where phi1, phi2 is Element of S -formulasOfMaxDepth m : S1[] } & z = [xx,yy] ) by ZFMISC_1:def 2;
reconsider x = xx as Element of U -InterpretersOf S by A7;
consider phi1, phi2 being Element of S -formulasOfMaxDepth m such that
A8: yy = H1(phi1,phi2) by A7;
reconsider phi11 = phi1, phi22 = phi2 as string of S ;
(<*()*> ^ phi11) ^ phi22 is string of S ;
then reconsider y = yy as string of S by A8;
( [x,phi1] in dom Fmm & [x,phi2] in dom Fmm ) by A1;
then [x,y] in dom (NorIterator ((S,U) -TruthEval m)) by ;
hence z in dom (NorIterator ((S,U) -TruthEval m)) by A7; :: thesis: verum
end;
then [:(), { H1(phi1,phi2) where phi1, phi2 is Element of S -formulasOfMaxDepth m : S1[] } :] c= dom (NorIterator ((S,U) -TruthEval m)) ;
hence dom (NorIterator ((S,U) -TruthEval m)) = [:(),():] by A6; :: thesis: verum