theorem Th49: :: COMPLSP2:59

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