let z be complex number ; :: thesis: ( Re (z * z) = ((Re z) ^2 ) - ((Im z) ^2 ) & Im (z * z) = 2 * ((Re z) * (Im z)) )
thus Re (z * z) = ((Re z) ^2 ) - ((Im z) ^2 ) by Th24; :: thesis: Im (z * z) = 2 * ((Re z) * (Im z))
thus Im (z * z) = ((Re z) * (Im z)) + ((Re z) * (Im z)) by Th24
.= 2 * ((Re z) * (Im z)) ; :: thesis: verum