let F, G be PartFunc of (REAL 3),REAL; :: thesis: ( dom F = D & ( for u being Element of REAL 3 st u in D holds
F . u = partdiff (f,u,3) ) & dom G = D & ( for u being Element of REAL 3 st u in D holds
G . u = partdiff (f,u,3) ) implies F = G )
assume that
A5: ( dom F = D & ( for u being Element of REAL 3 st u in D holds
F . u = partdiff (f,u,3) ) ) and
A6: ( dom G = D & ( for u being Element of REAL 3 st u in D holds
G . u = partdiff (f,u,3) ) ) ; :: thesis: F = G

now :: thesis: for u being Element of REAL 3 st u in dom F holds
F . u = G . u

let u be Element of REAL 3; :: thesis: ( u in dom F implies F . u = G . u )
assume A7: u in dom F ; :: thesis: F . u = G . u
then F . u = partdiff (f,u,3) by A5;
hence F . u = G . u by A5, A6, A7; :: thesis: verum

end;

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