let m be Nat; :: thesis: for S being Language
for U being non empty set holds dom (ExIterator ((S,U) -TruthEval m)) = [:(U -InterpretersOf S),(m -ExFormulasOf S):]
let S be Language; :: thesis: for U being non empty set holds dom (ExIterator ((S,U) -TruthEval m)) = [:(U -InterpretersOf S),(m -ExFormulasOf S):]
let U be non empty set ; :: thesis: dom (ExIterator ((S,U) -TruthEval m)) = [:(U -InterpretersOf S),(m -ExFormulasOf 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 = ExIterator ((S,U) -TruthEval m);
set L = LettersOf S;
deffunc H₁( set , FinSequence) -> set = <*$1*> ^ $2;
defpred S₁[] means verum;
set A = { H₁(v,phi) where v is Element of LettersOf S, phi is Element of S -formulasOfMaxDepth m : S₁[] } ;
set LH = dom (ExIterator ((S,U) -TruthEval m));
set RH = [:(U -InterpretersOf S), { H₁(v,phi) where v is Element of LettersOf S, phi is Element of S -formulasOfMaxDepth m : S₁[] } :];
(S,U) -TruthEval m is Element of Funcs ([:(U -InterpretersOf S),(S -formulasOfMaxDepth m):],BOOLEAN) by Th8;
then reconsider Fmm = (S,U) -TruthEval m as Function of [:(U -InterpretersOf S),(S -formulasOfMaxDepth m):],BOOLEAN ;
A1: dom Fmm = [:(U -InterpretersOf S),(S -formulasOfMaxDepth m):] by FUNCT_2:def 1;
reconsider ITT = ExIterator ((S,U) -TruthEval m) as PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN ;
A2: [:(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 :: thesis: for z being object st z in dom (ExIterator ((S,U) -TruthEval m)) holds
z in [:(U -InterpretersOf S), { H₁(v,phi) where v is Element of LettersOf S, phi is Element of S -formulasOfMaxDepth m : S₁[] } :]

let z be object ; :: thesis: ( z in dom (ExIterator ((S,U) -TruthEval m)) implies z in [:(U -InterpretersOf S), { H₁(v,phi) where v is Element of LettersOf S, phi is Element of S -formulasOfMaxDepth m : S₁[] } :] )
assume A3: z in dom (ExIterator ((S,U) -TruthEval m)) ; :: thesis: z in [:(U -InterpretersOf S), { H₁(v,phi) where v is Element of LettersOf S, phi 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
A4: z = [x,y] by A2;
consider v being literal Element of S, w being string of S such that
A5: ( [x,w] in dom ((S,U) -TruthEval m) & y = <*v*> ^ w ) by Def16, A3, A4;
reconsider phi = w as Element of S -formulasOfMaxDepth m by A1, A5, ZFMISC_1:87;
reconsider vv = v as Element of LettersOf S by FOMODEL1:def 14;
y = <*vv*> ^ phi by A5;
then y in { H₁(v,phi) where v is Element of LettersOf S, phi is Element of S -formulasOfMaxDepth m : S₁[] } ;
hence z in [:(U -InterpretersOf S), { H₁(v,phi) where v is Element of LettersOf S, phi is Element of S -formulasOfMaxDepth m : S₁[] } :] by ZFMISC_1:def 2, A4; :: thesis: verum

end;

then A6: dom (ExIterator ((S,U) -TruthEval m)) c= [:(U -InterpretersOf S), { H₁(v,phi) where v is Element of LettersOf S, phi is Element of S -formulasOfMaxDepth m : S₁[] } :] ;

now :: thesis: for z being object st z in [:(U -InterpretersOf S), { H₁(v,phi) where v is Element of LettersOf S, phi is Element of S -formulasOfMaxDepth m : S₁[] } :] holds
z in dom (ExIterator ((S,U) -TruthEval m))

let z be object ; :: thesis: ( z in [:(U -InterpretersOf S), { H₁(v,phi) where v is Element of LettersOf S, phi is Element of S -formulasOfMaxDepth m : S₁[] } :] implies z in dom (ExIterator ((S,U) -TruthEval m)) )
assume z in [:(U -InterpretersOf S), { H₁(v,phi) where v is Element of LettersOf S, phi is Element of S -formulasOfMaxDepth m : S₁[] } :] ; :: thesis: z in dom (ExIterator ((S,U) -TruthEval m))
then consider xx, yy being object such that
A7: ( xx in U -InterpretersOf S & yy in { H₁(v,phi) where v is Element of LettersOf S, phi 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 A7;
consider vv being Element of LettersOf S, phi being Element of S -formulasOfMaxDepth m such that
A8: yy = H₁(vv,phi) by A7;
reconsider v = vv as literal Element of S ;
reconsider w = phi as string of S ;
( [x,phi] in dom ((S,U) -TruthEval m) & yy = <*v*> ^ w ) by A8, A1;
hence z in dom (ExIterator ((S,U) -TruthEval m)) by A7, Def16; :: thesis: verum

end;

then [:(U -InterpretersOf S), { H₁(v,phi) where v is Element of LettersOf S, phi is Element of S -formulasOfMaxDepth m : S₁[] } :] c= dom (ExIterator ((S,U) -TruthEval m)) ;
hence dom (ExIterator ((S,U) -TruthEval m)) = [:(U -InterpretersOf S),(m -ExFormulasOf S):] by A6; :: thesis: verum