set IT = I quotient E;

set O = OwnSymbolsOf S;

A1: for o being Element of OwnSymbolsOf S holds

( (I quotient E) . o is Interpreter of o, Class E & (I quotient E) . o is Function )

(I quotient E) . x is Function by A1;

hence for b_{1} being Function st b_{1} = I quotient E holds

b_{1} is S, Class E -interpreter-like
by A3, FUNCOP_1:def 6; :: thesis: verum

set O = OwnSymbolsOf S;

A1: for o being Element of OwnSymbolsOf S holds

( (I quotient E) . o is Interpreter of o, Class E & (I quotient E) . o is Function )

proof

A3:
for x being object st x in dom (I quotient E) holds
let o be Element of OwnSymbolsOf S; :: thesis: ( (I quotient E) . o is Interpreter of o, Class E & (I quotient E) . o is Function )

reconsider i = I . o as E -respecting Interpreter of o,U ;

A2: i quotient E is Interpreter of o, Class E ;

hence (I quotient E) . o is Interpreter of o, Class E by Def17; :: thesis: (I quotient E) . o is Function

thus (I quotient E) . o is Function by A2, Def17; :: thesis: verum

end;reconsider i = I . o as E -respecting Interpreter of o,U ;

A2: i quotient E is Interpreter of o, Class E ;

hence (I quotient E) . o is Interpreter of o, Class E by Def17; :: thesis: (I quotient E) . o is Function

thus (I quotient E) . o is Function by A2, Def17; :: thesis: verum

(I quotient E) . x is Function by A1;

now :: thesis: for o being own Element of S holds (I quotient E) . o is Interpreter of o, Class E

then
I quotient E is Interpreter of S, Class E
by FOMODEL2:def 3;let o be own Element of S; :: thesis: (I quotient E) . o is Interpreter of o, Class E

reconsider oo = o as Element of OwnSymbolsOf S by FOMODEL1:def 19;

(I quotient E) . oo is Interpreter of oo, Class E by A1;

hence (I quotient E) . o is Interpreter of o, Class E ; :: thesis: verum

end;reconsider oo = o as Element of OwnSymbolsOf S by FOMODEL1:def 19;

(I quotient E) . oo is Interpreter of oo, Class E by A1;

hence (I quotient E) . o is Interpreter of o, Class E ; :: thesis: verum

hence for b

b