for K being Field
for a being Element of K
for x being FinSequence of K holds
( - (a * x) = (- a) * x & - (a * x) = a * (- x) )