let F0, G0 be PartFunc of REAL,(REAL n); :: thesis: ( dom F0 = X & ( for x being Real st x in X holds
F0 . x = diff (f,x) ) & dom G0 = X & ( for x being Real st x in X holds
G0 . x = diff (f,x) ) implies F0 = G0 )
assume that
A6: dom F0 = X and
A7: for x being Real st x in X holds
F0 . x = diff (f,x) and
A8: dom G0 = X and
A9: for x being Real st x in X holds
G0 . x = diff (f,x) ; :: thesis: F0 = G0

now :: thesis: for x being Element of REAL st x in dom F0 holds
F0 . x = G0 . x

let x be Element of REAL ; :: thesis: ( x in dom F0 implies F0 . x = G0 . x )
assume A10: x in dom F0 ; :: thesis: F0 . x = G0 . x
then F0 . x = diff (f,x) by A6, A7;
hence F0 . x = G0 . x by A6, A9, A10; :: thesis: verum

end;

hence F0 = G0 by A6, A8, PARTFUN1:5; :: thesis: verum