theorem Th18: :: MATRIXJ1:18

for D being non empty set
for F1, F2 being FinSequence_of_Matrix of D holds Width (F1 ^ F2) = (Width F1) ^ (Width F2)