let F, H be PartFunc of [:X,Y:],(R_NormSpace_of_BoundedLinearOperators (X,W)); ( dom F = Z & ( for z being Point of [:X,Y:] st z in Z holds
F /. z = partdiff`1 (f,z) ) & dom H = Z & ( for z being Point of [:X,Y:] st z in Z holds
H /. z = partdiff`1 (f,z) ) implies F = H )
assume that
A7:
dom F = Z
and
A8:
for x being Point of [:X,Y:] st x in Z holds
F /. x = partdiff`1 (f,x)
and
A9:
dom H = Z
and
A10:
for x being Point of [:X,Y:] st x in Z holds
H /. x = partdiff`1 (f,x)
; F = H
hence
F = H
by A7, A9, PARTFUN2:1; verum