let x be FinSequence of COMPLEX ; :: thesis: ( Re (<i> * x) = - (Im x) & Im (<i> * x) = Re x )
A1: len (x *') = len x by Def1;
A2: Im (<i> * x) = ((- (1 / 2)) * <i>) * ((<i> * x) - ((- <i>) * (x *'))) by Th13, COMPLEX1:31
.= ((- (1 / 2)) * <i>) * ((<i> * x) + (- (- (<i> * (x *'))))) by Th45
.= ((- (1 / 2)) * <i>) * (<i> * (x + (x *'))) by A1, Th25
.= (((- (1 / 2)) * <i>) * <i>) * (x + (x *')) by Th44
.= Re x ;
Re (<i> * x) = (1 / 2) * ((<i> * x) + ((- <i>) * (x *'))) by Th13, COMPLEX1:31
.= (1 / 2) * ((<i> * x) - (<i> * (x *'))) by Th45
.= (1 / 2) * (<i> * (x - (x *'))) by A1, Th36
.= ((1 / 2) * <i>) * (x - (x *')) by Th44
.= ((- 1) * ((- (1 / 2)) * <i>)) * (x - (x *'))
.= - (Im x) by Th44 ;
hence ( Re (<i> * x) = - (Im x) & Im (<i> * x) = Re x ) by A2; :: thesis: verum