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 & ( for x being Real st x in X holds
F . x = diff f,x ) ) and
A6: ( dom G = X & ( 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 A7: x in dom F ; :: thesis: F . x = G . x
then F . x = diff f,x by A5;
hence F . x = G . x by A5, A6, A7; :: thesis: verum

end;

hence F = G by A5, A6, PARTFUN1:34; :: thesis: verum