let H1, H2 be Function of X,(- Y); ( ( 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)
; H1 = H2
for x being object st x in X holds
H1 . x = H2 . x
proof
let x be
object ;
( x in X implies H1 . x = H2 . x )
assume
x in X
;
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
;
verum
end;
hence
H1 = H2
by FUNCT_2:12; verum