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