let x, y be Complex; :: thesis: |.(x .|. y).| = |.x.| * |.y.|
thus |.(x .|. y).| = |.x.| * |.(y *').| by COMPLEX1:65
.= |.x.| * |.y.| by COMPLEX1:53 ; :: thesis: verum