:: deftheorem Def20 defines -TruthEval FOMODEL2:def 21 :
for S being Language
for m being Nat
for U being non empty set
for b₄ being Element of PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN) holds
( b₄ = (S,U) -TruthEval m iff for mm being Element of NAT st m = mm holds
b₄ = ((S,U) -TruthEval) . mm );