let F, G be PartFunc of S,(R_NormSpace_of_BoundedLinearOperators (S,T)); :: thesis: ( dom F = X & ( for x being Point of S st x in X holds
F /. x = diff (f,x) ) & dom G = X & ( for x being Point of S st x in X holds
G /. x = diff (f,x) ) implies F = G )
assume that
A6: dom F = X and
A7: for x being Point of S st x in X holds
F /. x = diff (f,x) and
A8: dom G = X and
A9: for x being Point of S st x in X holds
G /. x = diff (f,x) ; :: thesis: F = G

now :: thesis: for x being Point of S st x in dom F holds
F /. x = G /. x

let x be Point of S; :: thesis: ( x in dom F implies F /. x = G /. x )
assume A10: x in dom F ; :: thesis: F /. x = G /. x
then F /. x = diff (f,x) by A6, A7;
hence F /. x = G /. x by A6, A9, A10; :: thesis: verum

end;

hence F = G by A6, A8, PARTFUN2:1; :: thesis: verum