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

let x be 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:34; :: thesis: verum