set O = OwnSymbolsOf S;
set IT0 = I quotient E;
defpred S₁[ Function] means ( dom $1 = OwnSymbolsOf S & ( for o being own Element of S holds $1 . o = (I . o) quotient E ) );
let IT be Function; :: thesis: ( IT = I quotient E iff ( dom IT = OwnSymbolsOf S & ( for o being own Element of S holds IT . o = (I . o) quotient E ) ) )
thus ( IT = I quotient E implies S₁[IT] ) :: thesis: ( dom IT = OwnSymbolsOf S & ( for o being own Element of S holds IT . o = (I . o) quotient E ) implies IT = I quotient E )

proof

assume C0: IT = I quotient E ; :: thesis: S₁[IT]
hence dom IT = OwnSymbolsOf S by DefQuot3; :: thesis: for o being own Element of S holds IT . o = (I . o) quotient E

now

let o be own Element of S; :: thesis: IT . o = (I . o) quotient E
reconsider oo = o as Element of OwnSymbolsOf S by FOMODEL1:def 19;
(I quotient E) . oo = (I . oo) quotient E by DefQuot3;
hence IT . o = (I . o) quotient E by C0; :: thesis: verum

end;

hence for o being own Element of S holds IT . o = (I . o) quotient E ; :: thesis: verum

end;

assume B0: S₁[IT] ; :: thesis: IT = I quotient E
for o being Element of OwnSymbolsOf S holds IT . o = (I . o) quotient E by B0;
hence IT = I quotient E by B0, DefQuot3; :: thesis: verum