for x, y being real-valued FinSequence st len x = len y holds
|.|(x,y)|.| <= |.x.| * |.y.|