set O = OwnSymbolsOf S;

set IT = (S,X) -freeInterpreter ;

_{1} being Function st b_{1} = (S,X) -freeInterpreter holds

b_{1} is Function-yielding
by FUNCOP_1:def 6; :: thesis: verum

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

hence
for b((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;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

b