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