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 b1 being Function st b1 = (S,X) -freeInterpreter holds
b1 is Function-yielding by FUNCOP_1:def 6; :: thesis: verum