:: deftheorem Def16 defines ExIterator FOMODEL2:def 17 :
for S being Language
for U being non empty set
for g being Element of PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN)
for b₄ being PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN holds
( b₄ = ExIterator g iff ( ( for x being Element of U -InterpretersOf S
for y being Element of ((AllSymbolsOf S) *) \ {{}} holds
( [x,y] in dom b₄ iff ex v being literal Element of S ex w being string of S st
( [x,w] in dom g & y = <*v*> ^ w ) ) ) & ( for x being Element of U -InterpretersOf S
for y being Element of ((AllSymbolsOf S) *) \ {{}} st [x,y] in dom b₄ holds
b₄ . (x,y) = g -ExFunctor (x,y) ) ) );