reconsider m9 = m, n9 = n as Element of NAT by ORDINAL1:def 12;
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_0: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