set O = OwnSymbolsOf S;

set IT0 = I quotient E;

defpred S_{1}[ 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_{1}[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 )_{1}[IT]
; :: thesis: IT = I quotient E

for o being Element of OwnSymbolsOf S holds IT . o = (I . o) quotient E by A2;

hence IT = I quotient E by A2, Def17; :: thesis: verum

set IT0 = I quotient E;

defpred S

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

proof

assume A2:
S
assume A1:
IT = I quotient E
; :: thesis: S_{1}[IT]

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

end;hence dom IT = OwnSymbolsOf S by Def17; :: thesis: for o being own Element of S holds IT . o = (I . o) quotient E

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

hence
for o being own Element of S holds IT . o = (I . o) quotient E
; :: thesis: verumlet 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 Def17;

hence IT . o = (I . o) quotient E by A1; :: thesis: verum

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

(I quotient E) . oo = (I . oo) quotient E by Def17;

hence IT . o = (I . o) quotient E by A1; :: thesis: verum

for o being Element of OwnSymbolsOf S holds IT . o = (I . o) quotient E by A2;

hence IT = I quotient E by A2, Def17; :: thesis: verum