set TT = AllTermsOf S;
set E = (X,D1) -termEq ;
set I = (S,X) -freeInterpreter ;
now :: thesis: for o being own Element of S holds ((S,X) -freeInterpreter) . o is (X,D1) -termEq -respecting
let o be own Element of S; :: thesis: ((S,X) -freeInterpreter) . o is (X,D1) -termEq -respecting
((S,X) -freeInterpreter) . o = X -freeInterpreter o by FOMODEL3:def 4;
hence ((S,X) -freeInterpreter) . o is (X,D1) -termEq -respecting ; :: thesis: verum
end;
hence for b1 being S, AllTermsOf S -interpreter-like Function st b1 = (S,X) -freeInterpreter holds
b1 is (X,D1) -termEq -respecting ; :: thesis: verum