deffunc H₁( set , set ) -> Element of D = M * (nt . $1),(mt . $2);
reconsider m' = m, n' = n as Element of NAT by ORDINAL1:def 13;
ex S being Matrix of n',m',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 n',m',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