theorem :: COMPLEX1:82

for z1, z2 being Complex holds z1 * z2 = (((Re z1) * (Re z2)) - ((Im z1) * (Im z2))) + ((((Re z1) * (Im z2)) + ((Re z2) * (Im z1))) * <i>)