let F0, G0 be PartFunc of REAL,(REAL n); :: 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

A6: dom F0 = X and

A7: for x being Real st x in X holds

F0 . x = diff (f,x) and

A8: dom G0 = X and

A9: for x being Real st x in X holds

G0 . x = diff (f,x) ; :: thesis: F0 = G0

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

A6: dom F0 = X and

A7: for x being Real st x in X holds

F0 . x = diff (f,x) and

A8: dom G0 = X and

A9: 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

hence
F0 = G0
by A6, A8, PARTFUN1:5; :: thesis: verumF0 . x = G0 . x

let x be Element of REAL ; :: thesis: ( x in dom F0 implies F0 . x = G0 . x )

assume A10: x in dom F0 ; :: thesis: F0 . x = G0 . x

then F0 . x = diff (f,x) by A6, A7;

hence F0 . x = G0 . x by A6, A9, A10; :: thesis: verum

end;assume A10: x in dom F0 ; :: thesis: F0 . x = G0 . x

then F0 . x = diff (f,x) by A6, A7;

hence F0 . x = G0 . x by A6, A9, A10; :: thesis: verum