let z be Complex; :: 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 Th9; :: thesis: Im (z * z) = 2 * ((Re z) * (Im z))
thus Im (z * z) = ((Re z) * (Im z)) + ((Re z) * (Im z)) by Th9
.= 2 * ((Re z) * (Im z)) ; :: thesis: verum