theorem Th53: :: MATRIXC1:55

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