theorem :: MATRIX_0:55

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