set IT = (S,X) -freeInterpreter ;
set A = AllTermsOf S;
for s being own Element of S holds ((S,X) -freeInterpreter) . s is Interpreter of s, AllTermsOf S

proof

let s be own Element of S; :: thesis: ((S,X) -freeInterpreter) . s is Interpreter of s, AllTermsOf S
X -freeInterpreter s is Interpreter of s, AllTermsOf S ;
hence ((S,X) -freeInterpreter) . s is Interpreter of s, AllTermsOf S by Def4; :: thesis: verum

end;

hence (S,X) -freeInterpreter is Interpreter of S, AllTermsOf S by FOMODEL2:def 3; :: thesis: verum