:: deftheorem Def4 defines -freeInterpreter FOMODEL3:def 4 :
for S being Language
for X being set
for b₃ being Function holds
( b₃ = (S,X) -freeInterpreter iff ( dom b₃ = OwnSymbolsOf S & ( for s being own Element of S holds b₃ . s = X -freeInterpreter s ) ) );