let z be Element of COMPLEX ; :: thesis: ( z .|. z = ((Re z) * (Re z)) + ((Im z) * (Im z)) & z .|. z = ((Re z) ^2 ) + ((Im z) ^2 ) )
thus z .|. z = (((Re z) * (Re z)) + ((Im z) * (Im z))) + (((- ((Im z) * (Re z))) + ((Im z) * (Re z))) * <i> ) by Th42
.= ((Re z) * (Re z)) + ((Im z) * (Im z)) ; :: thesis: z .|. z = ((Re z) ^2 ) + ((Im z) ^2 )
hence z .|. z = ((Re z) ^2 ) + ((Im z) ^2 ) ; :: thesis: verum