for x, y being FinSequence of REAL st len x = len y holds
FR2FC (mlt (x,y)) = mlt ((FR2FC x),(FR2FC y)) by Th35;