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_{1}( Element of OwnSymbolsOf S) -> set = (I . $1) quotient E;

assume A2: ( dom IT1 = OwnSymbolsOf S & ( for o being Element of OwnSymbolsOf S holds IT1 . o = H_{1}(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 A3: ( dom IT2 = OwnSymbolsOf S & ( for o being Element of OwnSymbolsOf S holds IT2 . o = H_{1}(o) ) )
; :: thesis: IT1 = IT2

( dom IT1 = dom IT2 & ( for x being object st x in dom IT1 holds

IT1 . x = IT2 . x ) )

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

assume A2: ( dom IT1 = OwnSymbolsOf S & ( for o being Element of OwnSymbolsOf S holds IT1 . o = H

assume A3: ( dom IT2 = OwnSymbolsOf S & ( for o being Element of OwnSymbolsOf S holds IT2 . o = H

( dom IT1 = dom IT2 & ( for x being object st x in dom IT1 holds

IT1 . x = IT2 . x ) )

proof

hence
IT1 = IT2
by FUNCT_1:2; :: thesis: verum
thus
dom IT1 = dom IT2
by A2, A3; :: thesis: for x being object st x in dom IT1 holds

IT1 . x = IT2 . x

let x be object ; :: 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 A2;

IT1 . o = H_{1}(o)
by A2

.= IT2 . o by A3 ;

hence IT1 . x = IT2 . x ; :: thesis: verum

end;IT1 . x = IT2 . x

let x be object ; :: 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 A2;

IT1 . o = H

.= IT2 . o by A3 ;

hence IT1 . x = IT2 . x ; :: thesis: verum