set EQ = TheEqSymbOf S;
set g = (TheEqSymbOf S) .--> (U -deltaInterpreter);
set O = OwnSymbolsOf S;
set A = AtomicFormulaSymbolsOf S;

now

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)) by FUNCOP_1:13;
then (I ===) . s = I . s by FUNCT_4:11;
hence (I ===) . s is Interpreter of s,U ; :: thesis: verum

end;

hence I === is Interpreter of S,U by DefInterpreter2; :: according to FOMODEL2:def 4 :: thesis: I === is Function-yielding
thus I === is Function-yielding ; :: thesis: verum