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: Re (<i> * x) = (1 / 2) * ((<i> * x) + ((- <i> ) * (x *' ))) by Th17, COMPLEX1:116
.= (1 / 2) * ((<i> * x) - (<i> * (x *' ))) by Th54
.= (1 / 2) * (<i> * (x - (x *' ))) by A1, Th43
.= ((1 / 2) * <i> ) * (x - (x *' )) by Th53
.= ((- 1) * ((- (1 / 2)) * <i> )) * (x - (x *' ))
.= - (Im x) by Th53 ;
Im (<i> * x) = ((- (1 / 2)) * <i> ) * ((<i> * x) - ((- <i> ) * (x *' ))) by Th17, COMPLEX1:116
.= ((- (1 / 2)) * <i> ) * ((<i> * x) + (- (- (<i> * (x *' ))))) by Th54
.= ((- (1 / 2)) * <i> ) * (<i> * (x + (x *' ))) by A1, Th30
.= (((- (1 / 2)) * <i> ) * <i> ) * (x + (x *' )) by Th53
.= Re x ;
hence ( Re (<i> * x) = - (Im x) & Im (<i> * x) = Re x ) by A2; :: thesis: verum