for x, y being FinSequence of REAL st ( for i being Nat st i in dom x holds
x . i >= 0 ) & ( for i being Nat st i in dom y holds
y . i >= 0 ) holds
for k being Nat st k in dom (mlt (x,y)) holds
(mlt (x,y)) . k >= 0