let H1, H2 be Function of X,(- Y); :: thesis: ( ( for x being Element of X holds H1 . x = - (F . x) ) & ( for x being Element of X holds H2 . x = - (F . x) ) implies H1 = H2 )
assume that
A3: for x being Element of X holds H1 . x = - (F . x) and
A4: for x being Element of X holds H2 . x = - (F . x) ; :: thesis: H1 = H2
for x being object st x in X holds
H1 . x = H2 . x

proof

let x be object ; :: thesis: ( x in X implies H1 . x = H2 . x )
assume x in X ; :: thesis: H1 . x = H2 . x
then reconsider x = x as Element of X ;
H1 . x = - (F . x) by A3
.= H2 . x by A4 ;
hence H1 . x = H2 . x ; :: thesis: verum

end;

hence H1 = H2 by FUNCT_2:12; :: thesis: verum