let z1, z2 be Complex; :: thesis: z1 * z2 = (((Re z1) * (Re z2)) - ((Im z1) * (Im z2))) + ((((Re z1) * (Im z2)) + ((Re z2) * (Im z1))) * <i>)
z1 * z2 = [*(((Re z1) * (Re z2)) - ((Im z1) * (Im z2))),(((Re z1) * (Im z2)) + ((Re z2) * (Im z1)))*] by Lm16;
hence z1 * z2 = (((Re z1) * (Re z2)) - ((Im z1) * (Im z2))) + ((((Re z1) * (Im z2)) + ((Re z2) * (Im z1))) * <i>) by Lm21; :: thesis: verum