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 )
proof
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;
A3: for x being object st x in dom (I quotient E) holds
(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
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;
then I quotient E is Interpreter of S, Class E by FOMODEL2:def 3;
hence for b1 being Function st b1 = I quotient E holds
b1 is S, Class E -interpreter-like by A3, FUNCOP_1:def 6; :: thesis: verum