let x, y be Element of COMPLEX ; :: thesis: |.(x .|. y).| = |.x.| * |.y.|
thus |.(x .|. y).| = |.x.| * |.(y *' ).| by COMPLEX1:151
.= |.x.| * |.y.| by COMPLEX1:139 ; :: thesis: verum