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

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

hence
F = G
by A5, A7, PARTFUN1:5; :: thesis: verumF . 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;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