set EQ = TheEqSymbOf S;

set g = (TheEqSymbOf S) .--> (U -deltaInterpreter);

set O = OwnSymbolsOf S;

set A = AtomicFormulaSymbolsOf S;

thus I === is Function-yielding ; :: thesis: verum

set g = (TheEqSymbOf S) .--> (U -deltaInterpreter);

set O = OwnSymbolsOf S;

set A = AtomicFormulaSymbolsOf S;

now :: thesis: for s being own Element of S holds (I ===) . s is Interpreter of s,U

hence
I === is Interpreter of S,U
by Def3; :: according to FOMODEL2:def 4 :: thesis: I === is Function-yielding let s be own Element of S; :: thesis: (I ===) . s is Interpreter of s,U

s in OwnSymbolsOf S by FOMODEL1:def 19;

then not s in (AtomicFormulaSymbolsOf S) \ (OwnSymbolsOf S) by XBOOLE_0:def 5;

then not s in {(TheEqSymbOf S)} by FOMODEL1:9;

then not s in dom ((TheEqSymbOf S) .--> (U -deltaInterpreter)) ;

then (I ===) . s = I . s by FUNCT_4:11;

hence (I ===) . s is Interpreter of s,U ; :: thesis: verum

end;s in OwnSymbolsOf S by FOMODEL1:def 19;

then not s in (AtomicFormulaSymbolsOf S) \ (OwnSymbolsOf S) by XBOOLE_0:def 5;

then not s in {(TheEqSymbOf S)} by FOMODEL1:9;

then not s in dom ((TheEqSymbOf S) .--> (U -deltaInterpreter)) ;

then (I ===) . s = I . s by FUNCT_4:11;

hence (I ===) . s is Interpreter of s,U ; :: thesis: verum

thus I === is Function-yielding ; :: thesis: verum