reconsider m9 = m, n9 = n as Element of NAT by ORDINAL1:def 12;
deffunc H1( 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) = H1(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) = H1(i,j)
;
reconsider S = S as Matrix of n,m,D ;
take
S
; 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; verum