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
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 Def3;
hence for b₁ being Function st b₁ = I | (OwnSymbolsOf S) holds
b₁ is S,U -interpreter-like by Def4; :: thesis: verum