set A = AllTermsOf S;
set n = abs (ar s);
set SS = AllSymbolsOf S;
set XF = X -freeInterpreter s;
set AF = AtomicFormulasOf S;
reconsider Ss = ((AllSymbolsOf S) *) \ {{}} as Subset of ((AllSymbolsOf S) *) ;
(abs (ar s)) -tuples_on (AllTermsOf S) c= (AllTermsOf S) * by FINSEQ_2:142;
then (abs (ar s)) -tuples_on (AllTermsOf S) c= Ss * by XBOOLE_1:1;
then reconsider f = (s -compound) | ((abs (ar s)) -tuples_on (AllTermsOf S)) as Function of ((abs (ar s)) -tuples_on (AllTermsOf S)),(((AllSymbolsOf S) *) \ {{}}) by FUNCT_2:32;

per cases ( s is relational or not s is relational ) ;

suppose C1: s is relational ; :: thesis: X -freeInterpreter s is Interpreter of s, AllTermsOf S

then reconsider ss = s as relational Element of S ;
(ss -compound) | ((abs (ar ss)) -tuples_on (AllTermsOf S)) is AtomicFormulasOf S -valued ;
then rng f c= AtomicFormulasOf S by RELAT_1:def 19;
then reconsider ff = f as Function of ((abs (ar s)) -tuples_on (AllTermsOf S)),(AtomicFormulasOf S) by RELSET_1:6;
reconsider g = chi (X,(AtomicFormulasOf S)) as Function of (AtomicFormulasOf S),BOOLEAN ;
g * ff is Function of ((abs (ar s)) -tuples_on (AllTermsOf S)),BOOLEAN ;
then X -freeInterpreter s is Function of ((abs (ar s)) -tuples_on (AllTermsOf S)),BOOLEAN by C1, DefFreeInt1;
hence X -freeInterpreter s is Interpreter of s, AllTermsOf S by C1, FOMODEL2:def 2; :: thesis: verum

end;

suppose C1: not s is relational ; :: thesis: X -freeInterpreter s is Interpreter of s, AllTermsOf S

then reconsider ss = s as non relational ofAtomicFormula Element of S ;
(ss -compound) | ((abs (ar ss)) -tuples_on (AllTermsOf S)) is AllTermsOf S -valued ;
then rng f c= AllTermsOf S by RELAT_1:def 19;
then f is Function of ((abs (ar s)) -tuples_on (AllTermsOf S)),(AllTermsOf S) by RELSET_1:6;
then X -freeInterpreter s is Function of ((abs (ar s)) -tuples_on (AllTermsOf S)),(AllTermsOf S) by C1, DefFreeInt1;
hence X -freeInterpreter s is Interpreter of s, AllTermsOf S by C1, FOMODEL2:def 2; :: thesis: verum

end;

end;