for K being Field
for x, y being FinSequence of K
for a being Element of K st len x = len y holds
|((a * x),y)| = a * |(x,y)|