theorem Th50: :: COMPLSP2:60

for x, y being FinSequence of COMPLEX st len x = len y holds
|(x,(<i> * y))| = - (<i> * |(x,y)|)