theorem Th37: :: MATRIXC1:39
for x, y being FinSequence of COMPLEX st len x = len y holds
|(x,y)| = Sum (mlt (x,(y *')))