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

now

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

end;

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