theorem Th13: :: MATRIX_3:13

for K being Ring
for p, q being FinSequence of K holds len (mlt (p,q)) = min ((len p),(len q))