let F0, G0 be PartFunc of REAL, the carrier of F; :: 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
A5: dom F0 = X and
A6: for x being Real st x in X holds
F0 . x = diff (f,x) and
A7: dom G0 = X and
A8: 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 A9: x in dom F0 ; :: thesis: F0 . x = G0 . x
then F0 . x = diff (f,x) by A5, A6;
hence F0 . x = G0 . x by A5, A8, A9; :: thesis: verum

end;

hence F0 = G0 by A5, A7, PARTFUN1:5; :: thesis: verum