let z1, z2 be complex number ; :: thesis: ( Re (z1 * z2) = ((Re z1) * (Re z2)) - ((Im z1) * (Im z2)) & Im (z1 * z2) = ((Re z1) * (Im z2)) + ((Re z2) * (Im z1)) )
( z1 in COMPLEX & z2 in COMPLEX ) by XCMPLX_0:def 2;
then z1 * z2 = [*(((Re z1) * (Re z2)) - ((Im z1) * (Im z2))),(((Re z1) * (Im z2)) + ((Re z2) * (Im z1)))*] by Lm16;
hence ( Re (z1 * z2) = ((Re z1) * (Re z2)) - ((Im z1) * (Im z2)) & Im (z1 * z2) = ((Re z1) * (Im z2)) + ((Re z2) * (Im z1)) ) by Lm2; :: thesis: verum