theorem Th46: :: MATRIXJ1:46

for D being non empty set
for S being FinSequence_of_Square-Matrix of D holds Len S = Width S