set EQ = TheEqSymbOf S;
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

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;

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