let z1, z2 be Complex; :: thesis: ( Re z1 = 0 & Re z2 = 0 implies ( Re (z1 * z2) = - ((Im z1) * (Im z2)) & Im (z1 * z2) = 0 ) )
assume that
A1: Re z1 = 0 and
A2: Re z2 = 0 ; :: thesis: ( Re (z1 * z2) = - ((Im z1) * (Im z2)) & Im (z1 * z2) = 0 )
thus Re (z1 * z2) = ((Re z1) * (Re z2)) - ((Im z1) * (Im z2)) by Th9
.= - ((Im z1) * (Im z2)) by A1 ; :: thesis: Im (z1 * z2) = 0
thus Im (z1 * z2) = ((Re z1) * (Im z2)) + ((Re z2) * (Im z1)) by Th9
.= 0 by A1, A2 ; :: thesis: verum