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;

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 )
;

end;

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;(I ===) . ss is Interpreter of s,U ;

hence f . s is Interpreter of s,U by Def11; :: thesis: verum

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;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