theorem Th45: :: COMPLSP2:54

for x being FinSequence of COMPLEX
for c being Complex holds (- c) * x = - (c * x)