theorem :: FOMODEL2:12

for m being Nat
for S being Language
for U being non empty set holds dom (ExIterator ((S,U) -TruthEval m)) = [:(U -InterpretersOf S),(m -ExFormulasOf S):] by Lm19;