let F, G be PartFunc of (REAL m),REAL; :: thesis: ( dom F = Z & ( for x being Element of REAL m st x in Z holds
F /. x = partdiff (f,x,i) ) & dom G = Z & ( for x being Element of REAL m st x in Z holds
G /. x = partdiff (f,x,i) ) implies F = G )
assume that
A6: ( dom F = Z & ( for x being Element of REAL m st x in Z holds
F /. x = partdiff (f,x,i) ) ) and
A7: ( dom G = Z & ( for x being Element of REAL m st x in Z holds
G /. x = partdiff (f,x,i) ) ) ; :: thesis: F = G

now :: thesis: for x being Element of REAL m st x in dom F holds
F /. x = G /. x

let x be Element of REAL m; :: thesis: ( x in dom F implies F /. x = G /. x )
assume A8: x in dom F ; :: thesis: F /. x = G /. x
then F /. x = partdiff (f,x,i) by A6;
hence F /. x = G /. x by A6, A7, A8; :: thesis: verum

end;

hence F = G by A6, A7, PARTFUN2:1; :: thesis: verum