theorem Th21: :: MATRIXJ1:21

for n being Nat
for D being non empty set
for F1 being FinSequence_of_Matrix of D holds Width (F1 | n) = (Width F1) | n