theorem :: MATRIX_0:56

for D being non empty set
for M1, M2 being Matrix of D st width M1 > 0 & width M2 > 0 holds
( M1 = M2 iff ( M1 @ = M2 @ & width M1 = width M2 ) )