let F, H be PartFunc of (product G),(R_NormSpace_of_BoundedLinearOperators ((G . (In (i,(dom G)))),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
A7: dom F = X and
A8: for x being Point of (product G) st x in X holds
F /. x = partdiff (f,x,i) and
A9: dom H = X and
A10: for x being Point of (product G) st x in X holds
H /. x = partdiff (f,x,i) ; :: thesis: F = H
now :: thesis: for x being Point of (product G) st x in dom F holds
F /. x = H /. x
let x be Point of (product G); :: 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 (f,x,i) 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