let z1, z2 be Complex; :: thesis: z1 * z2 = [*(((Re z1) * (Re z2)) - ((Im z1) * (Im z2))),(((Re z1) * (Im z2)) + ((Re z2) * (Im z1)))*]
set z = [*(((Re z1) * (Re z2)) - ((Im z1) * (Im z2))),(((Re z1) * (Im z2)) + ((Re z2) * (Im z1)))*];
reconsider z9 = z1 * z2 as Element of COMPLEX by XCMPLX_0:def 2;
A1: Im [*(((Re z1) * (Re z2)) - ((Im z1) * (Im z2))),(((Re z1) * (Im z2)) + ((Re z2) * (Im z1)))*] = ((Re z1) * (Im z2)) + ((Re z2) * (Im z1)) by Lm2
.= Im z9 by Lm14 ;
Re [*(((Re z1) * (Re z2)) - ((Im z1) * (Im z2))),(((Re z1) * (Im z2)) + ((Re z2) * (Im z1)))*] = ((Re z1) * (Re z2)) - ((Im z1) * (Im z2)) by Lm2
.= Re z9 by Lm13 ;
hence z1 * z2 = [*(((Re z1) * (Re z2)) - ((Im z1) * (Im z2))),(((Re z1) * (Im z2)) + ((Re z2) * (Im z1)))*] by A1; :: thesis: verum