let F, G be PartFunc of (REAL-NS m),(R_NormSpace_of_BoundedLinearOperators (REAL-NS 1),(REAL-NS n)); :: thesis: ( dom F = X & ( for x being Point of (REAL-NS m) st x in X holds
F /. x = partdiff f,x,i ) & dom G = X & ( for x being Point of (REAL-NS m) st x in X holds
G /. x = partdiff f,x,i ) implies F = G )
assume that
A6: ( dom F = X & ( for x being Point of (REAL-NS m) st x in X holds
F /. x = partdiff f,x,i ) ) and
A7: ( dom G = X & ( for x being Point of (REAL-NS m) st x in X holds
G /. x = partdiff f,x,i ) ) ; :: thesis: F = G

now

let x be Point of (REAL-NS m); :: thesis: ( x in dom F implies F /. x = G /. x )
assume A8: x in dom F ; :: thesis: F /. x = G /. x
then F /. x = partdiff f,x,i by A6;
hence F /. x = G /. x by A6, A7, A8; :: thesis: verum

end;

hence F = G by A6, A7, PARTFUN2:3; :: thesis: verum