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