theorem Th56: :: COMPLSP2:67

for x1, x2 being FinSequence of COMPLEX st len x1 = len x2 holds
|((- x1),x2)| = - |(x1,x2)|