let F, H be PartFunc of [:X,Y:],(R_NormSpace_of_BoundedLinearOperators (X,W)); :: thesis: ( 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) ; :: thesis: F = H

now :: thesis: for x being Point of [:X,Y:] st x in dom F holds
F /. x = H /. x

let x be Point of [:X,Y:]; :: thesis: ( x in dom F implies F /. x = H /. x )
assume A11: x in dom F ; :: thesis: F /. x = H /. x
then F /. x = partdiff`1 (f,x) by A7, A8;
hence F /. x = H /. x by A7, A10, A11; :: thesis: verum

end;

hence F = H by A7, A9, PARTFUN2:1; :: thesis: verum