let z be 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 Th27
.= ((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