theorem Th30: :: COMPLEX2:32

for x, y being Complex holds |.(x .|. y).| = |.x.| * |.y.|