let M1, M2 be Matrix of m,n,F_Real; :: thesis: ( ( for i, j being Nat st i in Seg m & j in Seg n holds
M1 * (i,j) = partdiff (f,x,i,j) ) & ( for i, j being Nat st i in Seg m & j in Seg n holds
M2 * (i,j) = partdiff (f,x,i,j) ) implies M1 = M2 )
assume A3: for i, j being Nat st i in Seg m & j in Seg n holds
M1 * (i,j) = partdiff (f,x,i,j) ; :: thesis: ( ex i, j being Nat st
( i in Seg m & j in Seg n & not M2 * (i,j) = partdiff (f,x,i,j) ) or M1 = M2 )
assume A4: for i, j being Nat st i in Seg m & j in Seg n holds
M2 * (i,j) = partdiff (f,x,i,j) ; :: thesis: M1 = M2
A5: ( len M1 = m & width M1 = n & Indices M1 = [:(Seg m),(Seg n):] ) by MATRIX_0:23;
A6: ( len M2 = m & width M2 = n & Indices M2 = [:(Seg m),(Seg n):] ) by MATRIX_0:23;
for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) = M2 * (i,j)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices M1 implies M1 * (i,j) = M2 * (i,j) )
assume [i,j] in Indices M1 ; :: thesis: M1 * (i,j) = M2 * (i,j)
then A7: ( i in Seg m & j in Seg n ) by A5, ZFMISC_1:87;
then M1 * (i,j) = partdiff (f,x,i,j) by A3;
hence M1 * (i,j) = M2 * (i,j) by A4, A7; :: thesis: verum

end;

hence M1 = M2 by A5, A6, MATRIX_0:21; :: thesis: verum