let z1, z2 be Element of 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 z' = z1 * z2 as Element of COMPLEX by XCMPLX_0:def 2;
A1: 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 Lm3
.= Re z' by Lm13 ;
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 Lm3
.= Im z' by Lm14 ;
hence z1 * z2 = [*(((Re z1) * (Re z2)) - ((Im z1) * (Im z2))),(((Re z1) * (Im z2)) + ((Re z2) * (Im z1)))*] by A1, Th9; :: thesis: verum