set IT = I quotient E;
set O = OwnSymbolsOf S;
B0: 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 ;
Z0: i quotient E is Interpreter of o, Class E ;
hence (I quotient E) . o is Interpreter of o, Class E by DefQuot3; :: thesis: (I quotient E) . o is Function
thus (I quotient E) . o is Function by Z0, DefQuot3; :: thesis: verum

end;

now

let x be set ; :: thesis: ( x in dom (I quotient E) implies (I quotient E) . x is Function )
assume x in dom (I quotient E) ; :: thesis: (I quotient E) . x is Function
then reconsider o = x as Element of OwnSymbolsOf S by DefQuot3;
(I quotient E) . o is Function by B0;
hence (I quotient E) . x is Function ; :: thesis: verum

end;

then B1: I quotient E is Function-yielding by FUNCOP_1:def 6;

now

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 B0;
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 b₁ being Function st b₁ = I quotient E holds
b₁ is S, Class E -interpreter-like by B1, FOMODEL2:def 4; :: thesis: verum