theorem :: MATRIX_0:27

for n, m being Nat
for D being non empty set
for M1, M2 being Matrix of n,m,D st ( for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) = M2 * (i,j) ) holds
M1 = M2