theorem :: MATRIX_0:45
for n, m being Nat
for D being non empty set
for M1 being Matrix of 0 ,n,D
for M2 being Matrix of 0 ,m,D holds M1 = M2