set O = OwnSymbolsOf S;
set AT = AllTermsOf S;
let IT1, IT2 be Function; :: thesis: ( dom IT1 = OwnSymbolsOf S & ( for o being Element of OwnSymbolsOf S holds IT1 . o = (I . o) quotient E ) & dom IT2 = OwnSymbolsOf S & ( for o being Element of OwnSymbolsOf S holds IT2 . o = (I . o) quotient E ) implies IT1 = IT2 )
deffunc H₁( Element of OwnSymbolsOf S) -> set = (I . $1) quotient E;
assume B1: ( dom IT1 = OwnSymbolsOf S & ( for o being Element of OwnSymbolsOf S holds IT1 . o = H₁(o) ) ) ; :: thesis: ( not dom IT2 = OwnSymbolsOf S or ex o being Element of OwnSymbolsOf S st not IT2 . o = (I . o) quotient E or IT1 = IT2 )
assume B2: ( dom IT2 = OwnSymbolsOf S & ( for o being Element of OwnSymbolsOf S holds IT2 . o = H₁(o) ) ) ; :: thesis: IT1 = IT2
( dom IT1 = dom IT2 & ( for x being set st x in dom IT1 holds
IT1 . x = IT2 . x ) )

proof

thus dom IT1 = dom IT2 by B1, B2; :: thesis: for x being set st x in dom IT1 holds
IT1 . x = IT2 . x
let x be set ; :: thesis: ( x in dom IT1 implies IT1 . x = IT2 . x )
assume x in dom IT1 ; :: thesis: IT1 . x = IT2 . x
then reconsider o = x as Element of OwnSymbolsOf S by B1;
IT1 . o = H₁(o) by B1
.= IT2 . o by B2 ;
hence IT1 . x = IT2 . x ; :: thesis: verum

end;

hence IT1 = IT2 by FUNCT_1:2; :: thesis: verum