set O = OwnSymbolsOf S;
set f = I | (OwnSymbolsOf S);
set D = dom (I | (OwnSymbolsOf S));
set C = U \/ BOOLEAN;

now

let s be own Element of S; :: thesis: (I | (OwnSymbolsOf S)) . s is Interpreter of s,U
s in OwnSymbolsOf S by FOMODEL1:def 19;
then (I | (OwnSymbolsOf S)) . s = I . s by 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 DefInterpreter2;
hence for b₁ being Function st b₁ = I | (OwnSymbolsOf S) holds
b₁ is S,U -interpreter-like by DefInterpreterLike; :: thesis: verum