defpred S₁[ Nat, Nat, object ] means $3 = partdiff (f,x,$1,$2);
A1: for i, j being Nat st [i,j] in [:(Seg m),(Seg n):] holds
ex y being Element of F_Real st S₁[i,j,y]

proof

let i, j be Nat; :: thesis: ( [i,j] in [:(Seg m),(Seg n):] implies ex y being Element of F_Real st S₁[i,j,y] )
partdiff (f,x,i,j) in REAL by XREAL_0:def 1;
hence ( [i,j] in [:(Seg m),(Seg n):] implies ex y being Element of F_Real st S₁[i,j,y] ) ; :: thesis: verum

end;

consider M being Matrix of m,n,F_Real such that
A2: for i, j being Nat st [i,j] in Indices M holds
S₁[i,j,M * (i,j)] from MATRIX_0:sch 2(A1);
take M ; :: thesis: for i, j being Nat st i in Seg m & j in Seg n holds
M * (i,j) = partdiff (f,x,i,j)
thus for i, j being Nat st i in Seg m & j in Seg n holds
M * (i,j) = partdiff (f,x,i,j) :: thesis: verum

proof

let i, j be Nat; :: thesis: ( i in Seg m & j in Seg n implies M * (i,j) = partdiff (f,x,i,j) )
assume ( i in Seg m & j in Seg n ) ; :: thesis: M * (i,j) = partdiff (f,x,i,j)
then [i,j] in [:(Seg m),(Seg n):] by ZFMISC_1:87;
then [i,j] in Indices M by MATRIX_0:23;
hence M * (i,j) = partdiff (f,x,i,j) by A2; :: thesis: verum

end;