:: deftheorem Def15 defines -ExFunctor FOMODEL2:def 16 :
for S being Language
for U being non empty set
for I being Element of U -InterpretersOf S
for f being PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN
for phi being Element of ((AllSymbolsOf S) *) \ {{}} holds
( ( ex u being Element of U ex v being literal Element of S st
( phi . 1 = v & f . (((v,u) ReassignIn I),(phi /^ 1)) = TRUE ) implies f -ExFunctor (I,phi) = TRUE ) & ( ( for u being Element of U
for v being literal Element of S holds
( not phi . 1 = v or not f . (((v,u) ReassignIn I),(phi /^ 1)) = TRUE ) ) implies f -ExFunctor (I,phi) = FALSE ) );