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

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

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

then reconsider ss = s as relational Element of S ;
(ss -compound) | (|.(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 (|.(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 (|.(ar s).| -tuples_on (AllTermsOf S)),BOOLEAN ;
then X -freeInterpreter s is Function of (|.(ar s).| -tuples_on (AllTermsOf S)),BOOLEAN by A1, Def3;
hence X -freeInterpreter s is Interpreter of s, AllTermsOf S by A1, FOMODEL2:def 2; :: thesis: verum

end;

suppose A2: 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) | (|.(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 (|.(ar s).| -tuples_on (AllTermsOf S)),(AllTermsOf S) by RELSET_1:6;
then X -freeInterpreter s is Function of (|.(ar s).| -tuples_on (AllTermsOf S)),(AllTermsOf S) by A2, Def3;
hence X -freeInterpreter s is Interpreter of s, AllTermsOf S by A2, FOMODEL2:def 2; :: thesis: verum

end;

end;