for x, y being FinSequence of REAL st len x = len y & ( for i being Element of NAT st i in Seg (len x) holds
( 0 <= x . i & x . i <= y . i ) ) holds
|.x.| <= |.y.|