let z1, z2 be Complex; :: thesis: (z1 * z2) *' = (z1 *') * (z2 *')
A1: ( Re (z1 *') = Re z1 & Re (z2 *') = Re z2 ) by Th27;
A2: ( Im (z1 *') = - (Im z1) & Im (z2 *') = - (Im z2) ) by Th27;
thus Re ((z1 * z2) *') = Re (z1 * z2) by Th27
.= ((Re (z1 *')) * (Re (z2 *'))) - ((- (Im (z1 *'))) * (- (Im (z2 *')))) by A1, A2, Th9
.= ((Re (z1 *')) * (Re (z2 *'))) - (- (- ((Im (z1 *')) * (Im (z2 *')))))
.= Re ((z1 *') * (z2 *')) by Th9 ; :: according to COMPLEX1:def 3 :: thesis: Im ((z1 * z2) *') = Im ((z1 *') * (z2 *'))
thus Im ((z1 * z2) *') = - (Im (z1 * z2)) by Th27
.= - (((Re (z1 *')) * (- (Im (z2 *')))) + ((Re (z2 *')) * (- (Im (z1 *'))))) by A1, A2, Th9
.= ((Re (z2 *')) * (Im (z1 *'))) + (- (- ((Re (z1 *')) * (Im (z2 *')))))
.= Im ((z1 *') * (z2 *')) by Th9 ; :: thesis: verum