set f = (S,X) -freeInterpreter ;
set U = AllTermsOf S;
set O = OwnSymbolsOf S;
dom ((S,X) -freeInterpreter) c= OwnSymbolsOf S by Def4;
then ((S,X) -freeInterpreter) | (OwnSymbolsOf S) = (S,X) -freeInterpreter by RELAT_1:68;
hence (S,X) -freeInterpreter is Element of (AllTermsOf S) -InterpretersOf S by FOMODEL2:2; :: thesis: verum