set O = OwnSymbolsOf S;

set f = I | (OwnSymbolsOf S);

set D = dom (I | (OwnSymbolsOf S));

set C = U \/ BOOLEAN;

hence for b_{1} being Function st b_{1} = I | (OwnSymbolsOf S) holds

b_{1} is S,U -interpreter-like
; :: thesis: verum

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

then
I | (OwnSymbolsOf S) is Interpreter of S,U
by Def3;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;(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

hence for b

b