theorem Th30: :: MATRPROB:30

for x, y being FinSequence of REAL st len x = len y holds
len (mlt (x,y)) = len x by FINSEQ_2:72;