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

now :: thesis: for x being Element of REAL st x in dom F holds
F . x = G . x

let x be Element of REAL ; :: thesis: ( x in dom F implies F . x = G . x )
assume A9: x in dom F ; :: thesis: F . x = G . x
then F . x = diff (f,x) by A5, A6;
hence F . x = G . x by A5, A8, A9; :: thesis: verum

end;

hence F = G by A5, A7, PARTFUN1:5; :: thesis: verum