let S be Language; :: thesis: for U being non empty set
for f being Function st f is S,U -interpreter-like holds
OwnSymbolsOf S c= dom f
let U be non empty set ; :: thesis: for f being Function st f is S,U -interpreter-like holds
OwnSymbolsOf S c= dom f
let f be Function; :: thesis: ( f is S,U -interpreter-like implies OwnSymbolsOf S c= dom f )
assume f is S,U -interpreter-like ; :: thesis: OwnSymbolsOf S c= dom f
then f is Interpreter of S,U by DefInterpreterLike;
hence OwnSymbolsOf S c= dom f by Lm2; :: thesis: verum