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 b₁ being S, AllTermsOf S -interpreter-like Function st b₁ = (S,X) -freeInterpreter holds
b₁ is (X,D1) -termEq -respecting ; :: thesis: verum