let F, G be PartFunc of (REAL m),(Funcs ((REAL m),(REAL n))); :: thesis: ( dom F = Z & ( for x being Element of REAL m st x in Z holds
F /. x = diff (f,x) ) & dom G = Z & ( for x being Element of REAL m st x in Z holds
G /. x = diff (f,x) ) implies F = G )
assume that
A7: dom F = Z and
A8: for x being Element of REAL m st x in Z holds
F /. x = diff (f,x) and
A9: dom G = Z and
A10: for x being Element of REAL m st x in Z holds
G /. x = diff (f,x) ; :: thesis: F = G
now :: thesis: for x being Element of REAL m st x in dom F holds
F /. x = G /. x
let x be Element of REAL m; :: thesis: ( x in dom F implies F /. x = G /. x )
assume A11: x in dom F ; :: thesis: F /. x = G /. x
then F /. x = diff (f,x) by A7, A8;
hence F /. x = G /. x by A7, A10, A11; :: thesis: verum
end;
hence F = G by A7, A9, PARTFUN2:1; :: thesis: verum