set O = OwnSymbolsOf S;
set IT0 = I quotient E;
defpred S1[ 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 S1[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 A1: IT = I quotient E ; :: thesis: S1[IT]
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
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 Def17;
hence IT . o = (I . o) quotient E by A1; :: thesis: verum
end;
hence for o being own Element of S holds IT . o = (I . o) quotient E ; :: thesis: verum
end;
assume A2: S1[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