reconsider m9 = m, n9 = n as Element of NAT by ORDINAL1:def 13;
deffunc H₁( set , set ) -> Element of D = M * (nt . $1),(mt . $2);
ex S being Matrix of n9,m9,D st
for i, j being Nat st [i,j] in Indices S holds
S * i,j = H₁(i,j) from MATRIX_1:sch 1();
then consider S being Matrix of n9,m9,D such that
A1: for i, j being Nat st [i,j] in Indices S holds
S * i,j = H₁(i,j) ;
reconsider S = S as Matrix of n,m,D ;
take S ; :: thesis: for i, j being Nat st [i,j] in Indices S holds
S * i,j = M * (nt . i),(mt . j)
thus for i, j being Nat st [i,j] in Indices S holds
S * i,j = M * (nt . i),(mt . j) by A1; :: thesis: verum