set a = the adicity of S;
set EQ = TheEqSymbOf S;
set d = U -deltaInterpreter ;
set g = (TheEqSymbOf S) .--> (U -deltaInterpreter);
set n = ar s;
set A = AtomicFormulaSymbolsOf S;
set O = OwnSymbolsOf S;
reconsider sss = s as Element of AtomicFormulaSymbolsOf S by FOMODEL1:def 20;
reconsider EQQ = TheEqSymbOf S as ofAtomicFormula Element of S ;
ar EQQ = - 2 by FOMODEL1:def 23;
then A1: |.(ar EQQ).| = - (- 2) by ABSVALUE:def 1
.= 2 ;
A2: f = I === by Def11;
per cases ( s is own or not s is own ) ;
suppose s is own ; :: thesis: f . s is Interpreter of s,U
then reconsider ss = s as own Element of S ;
(I ===) . ss is Interpreter of s,U ;
hence f . s is Interpreter of s,U by Def11; :: thesis: verum
end;
suppose not s is own ; :: thesis: f . s is Interpreter of s,U
then not sss in OwnSymbolsOf S ;
then sss in (AtomicFormulaSymbolsOf S) \ (OwnSymbolsOf S) by XBOOLE_0:def 5;
then sss in {(TheEqSymbOf S)} by FOMODEL1:9;
then s = TheEqSymbOf S by TARSKI:def 1;
then ( f . s is Function of (|.(ar s).| -tuples_on U),BOOLEAN & s is relational ) by A1, A2, FUNCT_7:94;
hence f . s is Interpreter of s,U by Def2; :: thesis: verum
end;
end;