set O = OwnSymbolsOf S;
set f = I | (OwnSymbolsOf S);
set D = dom (I | (OwnSymbolsOf S));
set C = U \/ BOOLEAN;
now :: thesis: for s being own Element of S holds (I | (OwnSymbolsOf S)) . s is Interpreter of s,U
let s be own Element of S; :: thesis: (I | (OwnSymbolsOf S)) . s is Interpreter of s,U
(I | (OwnSymbolsOf S)) . s = I . s by FOMODEL1:def 19, FUNCT_1:49;
hence (I | (OwnSymbolsOf S)) . s is Interpreter of s,U ; :: thesis: verum
end;
then I | (OwnSymbolsOf S) is Interpreter of S,U by Def3;
hence for b1 being Function st b1 = I | (OwnSymbolsOf S) holds
b1 is S,U -interpreter-like ; :: thesis: verum