set O = OwnSymbolsOf S;
set IT = (S,X) -freeInterpreter ;

now

let x be set ; :: thesis: ( x in dom ((S,X) -freeInterpreter) implies ((S,X) -freeInterpreter) . x is Function )
assume x in dom ((S,X) -freeInterpreter) ; :: thesis: ((S,X) -freeInterpreter) . x is Function
then x in OwnSymbolsOf S by DefFree1;
then reconsider s = x as own Element of S by FOMODEL1:def 19;
X -freeInterpreter s is Function ;
hence ((S,X) -freeInterpreter) . x is Function by DefFree1; :: thesis: verum

end;

hence for b₁ being Function st b₁ = (S,X) -freeInterpreter holds
b₁ is Function-yielding by FUNCOP_1:def 6; :: thesis: verum