let F, G be PartFunc of (REAL 2),REAL; :: thesis: ( dom F = Z & ( for z being Element of REAL 2 st z in Z holds

F . z = partdiff (f,z,1) ) & dom G = Z & ( for z being Element of REAL 2 st z in Z holds

G . z = partdiff (f,z,1) ) implies F = G )

assume that

A5: dom F = Z and

A6: for z being Element of REAL 2 st z in Z holds

F . z = partdiff (f,z,1) and

A7: dom G = Z and

A8: for z being Element of REAL 2 st z in Z holds

G . z = partdiff (f,z,1) ; :: thesis: F = G

F . z = partdiff (f,z,1) ) & dom G = Z & ( for z being Element of REAL 2 st z in Z holds

G . z = partdiff (f,z,1) ) implies F = G )

assume that

A5: dom F = Z and

A6: for z being Element of REAL 2 st z in Z holds

F . z = partdiff (f,z,1) and

A7: dom G = Z and

A8: for z being Element of REAL 2 st z in Z holds

G . z = partdiff (f,z,1) ; :: thesis: F = G

now :: thesis: for z being Element of REAL 2 st z in dom F holds

F . z = G . z

hence
F = G
by A5, A7, PARTFUN1:5; :: thesis: verumF . z = G . z

let z be Element of REAL 2; :: thesis: ( z in dom F implies F . z = G . z )

assume A9: z in dom F ; :: thesis: F . z = G . z

then F . z = partdiff (f,z,1) by A5, A6;

hence F . z = G . z by A5, A8, A9; :: thesis: verum

end;assume A9: z in dom F ; :: thesis: F . z = G . z

then F . z = partdiff (f,z,1) by A5, A6;

hence F . z = G . z by A5, A8, A9; :: thesis: verum