theorem Th52: :: MATRIXC1:54

for x, y being FinSequence of COMPLEX st len x = len y & 0 < len y holds
|(x,y)| = |(y,x)| *'