theorem :: MATRIXJ1:62

for K being Field
for G being FinSequence_of_Matrix of K
for p being FinSequence of K holds
( Len (mlt (p,G)) = Len G & Width (mlt (p,G)) = Width G )