theorem Th24: :: MATRIX_0:24
for n being Nat
for D being non empty set
for M being Matrix of n,D holds
( len M = n & width M = n & Indices M = [:(Seg n),(Seg n):] )