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

now :: thesis: for x being object st x in dom ((S,X) -freeInterpreter) holds
((S,X) -freeInterpreter) . x is Function

let x be object ; :: 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 Def4;
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 Def4; :: 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