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