theorem :: FOMODEL2:11

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