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 and

A7: for x being Point of (REAL-NS m) st x in X holds

F /. x = partdiff (f,x,i) and

A8: dom G = X and

A9: for x being Point of (REAL-NS m) st x in X holds

G /. x = partdiff (f,x,i) ; :: thesis: F = G

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 and

A7: for x being Point of (REAL-NS m) st x in X holds

F /. x = partdiff (f,x,i) and

A8: dom G = X and

A9: for x being Point of (REAL-NS m) st x in X holds

G /. x = partdiff (f,x,i) ; :: thesis: F = G

now :: thesis: for x being Point of (REAL-NS m) st x in dom F holds

F /. x = G /. x

hence
F = G
by A6, A8, PARTFUN2:1; :: thesis: verumF /. x = G /. x

let x be Point of (REAL-NS m); :: thesis: ( x in dom F implies F /. x = G /. x )

assume A10: x in dom F ; :: thesis: F /. x = G /. x

then F /. x = partdiff (f,x,i) by A6, A7;

hence F /. x = G /. x by A6, A9, A10; :: thesis: verum

end;assume A10: x in dom F ; :: thesis: F /. x = G /. x

then F /. x = partdiff (f,x,i) by A6, A7;

hence F /. x = G /. x by A6, A9, A10; :: thesis: verum