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 = hpartdiff31 f,u ) & dom G = D & ( for u being Element of REAL 3 st u in D holds
G . u = hpartdiff31 f,u ) implies F = G )
assume that
A6: ( dom F = D & ( for u being Element of REAL 3 st u in D holds
F . u = hpartdiff31 f,u ) ) and
A7: ( dom G = D & ( for u being Element of REAL 3 st u in D holds
G . u = hpartdiff31 f,u ) ) ; :: thesis: F = G

now

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

end;

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