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