let a be Element of COMPLEX ; :: thesis: for x being FinSequence of COMPLEX holds
( Re (a * x) = ((Re a) * (Re x)) - ((Im a) * (Im x)) & Im (a * x) = ((Im a) * (Re x)) + ((Re a) * (Im x)) )

let x be FinSequence of COMPLEX ; :: thesis: ( Re (a * x) = ((Re a) * (Re x)) - ((Im a) * (Im x)) & Im (a * x) = ((Im a) * (Re x)) + ((Re a) * (Im x)) )
reconsider z5 = Re a, z6 = Im a as Element of COMPLEX by XCMPLX_0:def 2;
A1: len (x *') = len x by Def1;
len (((1 / 2) * z5) * x) = len x by Th3;
then A2: len (((((1 / 2) * <i>) * z6) * x) + (((1 / 2) * z5) * x)) = len ((((1 / 2) * <i>) * z6) * x) by ;
A3: len (((1 / 2) * z5) * x) = len x by Th3;
A4: ( len (z5 * x) = len x & len ((<i> * z6) * x) = len x ) by Th3;
A5: (Re a) * (Re x) = (z5 * (1 / 2)) * (x + (x *')) by Th44
.= (((z5 * 1) / 2) * x) + (((z5 * 1) / 2) * (x *')) by ;
A6: ( len (Re x) = len x & len ((Re a) * (Re x)) = len (Re x) ) by ;
A7: ( len ((z5 - (z6 * <i>)) * (x *')) = len (x *') & len ((z5 + (<i> * z6)) * x) = len x ) by Th3;
A8: len (((- ((1 / 2) * <i>)) * z6) * (x *')) = len (x *') by Th3;
A9: (Im a) * (Im x) = (z6 * (- ((1 / 2) * <i>))) * (x - (x *')) by Th44
.= (((- ((1 / 2) * <i>)) * z6) * x) - (((- ((1 / 2) * <i>)) * z6) * (x *')) by ;
A10: len (((- ((1 / 2) * <i>)) * z6) * x) = len x by Th3;
A11: ( len (z5 * (x *')) = len (x *') & len ((z6 * <i>) * (x *')) = len (x *') ) by Th3;
A12: ( len (((1 / 2) * z5) * (x *')) = len (x *') & len ((((1 / 2) * <i>) * z6) * x) = len x ) by Th3;
A13: Re (a * x) = (1 / 2) * (((a *') * (x *')) + (a * x)) by Th13
.= (1 / 2) * (((a *') * (x *')) + ((z5 + (<i> * z6)) * x)) by COMPLEX1:13
.= (1 / 2) * (((z5 - (z6 * <i>)) * (x *')) + ((z5 + (<i> * z6)) * x)) by COMPLEX1:def 11
.= ((1 / 2) * ((z5 - (z6 * <i>)) * (x *'))) + ((1 / 2) * ((z5 + (<i> * z6)) * x)) by
.= ((1 / 2) * ((z5 - (z6 * <i>)) * (x *'))) + ((1 / 2) * ((z5 * x) + ((<i> * z6) * x))) by Th52
.= ((1 / 2) * ((z5 * (x *')) - ((z6 * <i>) * (x *')))) + ((1 / 2) * ((z5 * x) + ((<i> * z6) * x))) by Th53
.= ((1 / 2) * ((z5 * (x *')) - ((z6 * <i>) * (x *')))) + (((1 / 2) * (z5 * x)) + ((1 / 2) * ((<i> * z6) * x))) by
.= (((1 / 2) * (z5 * (x *'))) - ((1 / 2) * ((z6 * <i>) * (x *')))) + (((1 / 2) * (z5 * x)) + ((1 / 2) * ((<i> * z6) * x))) by
.= (((1 / 2) * (z5 * (x *'))) - ((1 / 2) * ((<i> * z6) * (x *')))) + (((1 / 2) * (z5 * x)) + (((1 / 2) * (<i> * z6)) * x)) by Th44
.= (((1 / 2) * (z5 * (x *'))) + (- ((((1 / 2) * <i>) * z6) * (x *')))) + (((1 / 2) * (z5 * x)) + ((((1 / 2) * <i>) * z6) * x)) by Th44
.= (((1 / 2) * (z5 * (x *'))) + ((- (((1 / 2) * <i>) * z6)) * (x *'))) + (((1 / 2) * (z5 * x)) + ((((1 / 2) * <i>) * z6) * x)) by Th45
.= ((((1 / 2) * z5) * (x *')) + (((- ((1 / 2) * <i>)) * z6) * (x *'))) + (((1 / 2) * (z5 * x)) + ((((1 / 2) * <i>) * z6) * x)) by Th44
.= ((((1 / 2) * z5) * x) + ((((1 / 2) * <i>) * z6) * x)) + ((((1 / 2) * z5) * (x *')) + (((- ((1 / 2) * <i>)) * z6) * (x *'))) by Th44
.= ((((((1 / 2) * <i>) * z6) * x) + (((1 / 2) * z5) * x)) + (((1 / 2) * z5) * (x *'))) + (((- ((1 / 2) * <i>)) * z6) * (x *')) by A1, A8, A12, A2, Th24
.= (((((1 / 2) * z5) * x) + (((1 / 2) * z5) * (x *'))) + ((- ((- ((1 / 2) * <i>)) * z6)) * x)) + (((- ((1 / 2) * <i>)) * z6) * (x *')) by A1, A3, A12, Th24
.= (((((1 / 2) * z5) * x) + (((1 / 2) * z5) * (x *'))) - (((- ((1 / 2) * <i>)) * z6) * x)) + (((- ((1 / 2) * <i>)) * z6) * (x *')) by Th45
.= ((Re a) * (Re x)) - ((Im a) * (Im x)) by A1, A5, A9, A6, A10, A8, Th33 ;
A14: len ((((1 / 2) * <i>) * z5) * (x *')) = len (x *') by Th3;
A15: (Im a) * (Re x) = (z6 * (1 / 2)) * (x + (x *')) by Th44
.= (((1 / 2) * z6) * x) + (((1 / 2) * z6) * (x *')) by ;
A16: ( len ((<i> * z6) * (x *')) = len (x *') & len ((- z5) * (x *')) = len (x *') ) by Th3;
A17: len ((1 / 2) * (z6 * x)) = len (z6 * x) by Th3;
A18: ( len (z6 * (x *')) = len (x *') & len ((1 / 2) * (z6 * (x *'))) = len (z6 * (x *')) ) by Th3;
then A19: len (((1 / 2) * (z6 * x)) + ((1 / 2) * (z6 * (x *')))) = len ((1 / 2) * (z6 * x)) by A1, A17, Th3, Th6;
A20: len (((- ((1 / 2) * <i>)) * z5) * x) = len x by Th3;
then A21: len (((1 / 2) * (z6 * x)) + (((- ((1 / 2) * <i>)) * z5) * x)) = len ((1 / 2) * (z6 * x)) by ;
A22: (Re a) * (Im x) = (z5 * (- ((1 / 2) * <i>))) * (x - (x *')) by Th44
.= (((- ((1 / 2) * <i>)) * z5) * x) - (((- ((1 / 2) * <i>)) * z5) * (x *')) by ;
A23: len (z6 * x) = len x by Th3;
( len ((a * x) *') = len (a * x) & len (- ((a * x) *')) = len ((a * x) *') ) by ;
then Im (a * x) = ((- ((1 / 2) * <i>)) * (- ((a * x) *'))) + ((- ((1 / 2) * <i>)) * (a * x)) by Th25
.= ((- ((1 / 2) * <i>)) * (- ((a *') * (x *')))) + ((- ((1 / 2) * <i>)) * (a * x)) by Th13
.= ((- ((1 / 2) * <i>)) * (- ((a *') * (x *')))) + ((- ((1 / 2) * <i>)) * ((z5 + (<i> * z6)) * x)) by COMPLEX1:13
.= ((- ((1 / 2) * <i>)) * (- ((z5 - (z6 * <i>)) * (x *')))) + ((- ((1 / 2) * <i>)) * ((z5 + (<i> * z6)) * x)) by COMPLEX1:def 11
.= ((- ((1 / 2) * <i>)) * ((- (z5 - (z6 * <i>))) * (x *'))) + ((- ((1 / 2) * <i>)) * ((z5 + (<i> * z6)) * x)) by Th45
.= ((- ((1 / 2) * <i>)) * (((- z5) + (z6 * <i>)) * (x *'))) + ((- ((1 / 2) * <i>)) * ((z5 + (<i> * z6)) * x))
.= ((- ((1 / 2) * <i>)) * (((- z5) * (x *')) + ((<i> * z6) * (x *')))) + ((- ((1 / 2) * <i>)) * ((z5 + (<i> * z6)) * x)) by Th52
.= ((- ((1 / 2) * <i>)) * (((- z5) * (x *')) + ((<i> * z6) * (x *')))) + ((- ((1 / 2) * <i>)) * ((z5 * x) + ((<i> * z6) * x))) by Th52
.= ((- ((1 / 2) * <i>)) * (((- z5) * (x *')) + ((<i> * z6) * (x *')))) + (((- ((1 / 2) * <i>)) * (z5 * x)) + ((- ((1 / 2) * <i>)) * ((<i> * z6) * x))) by
.= (((- ((1 / 2) * <i>)) * ((- z5) * (x *'))) + ((- ((1 / 2) * <i>)) * ((<i> * z6) * (x *')))) + (((- ((1 / 2) * <i>)) * (z5 * x)) + ((- ((1 / 2) * <i>)) * ((<i> * z6) * x))) by
.= ((((- ((1 / 2) * <i>)) * (- z5)) * (x *')) + ((- ((1 / 2) * <i>)) * ((<i> * z6) * (x *')))) + (((- ((1 / 2) * <i>)) * (z5 * x)) + ((- ((1 / 2) * <i>)) * ((<i> * z6) * x))) by Th44
.= ((((- ((1 / 2) * <i>)) * (- z5)) * (x *')) + ((- ((1 / 2) * <i>)) * (<i> * (z6 * (x *'))))) + (((- ((1 / 2) * <i>)) * (z5 * x)) + ((- ((1 / 2) * <i>)) * ((<i> * z6) * x))) by Th44
.= ((((- ((1 / 2) * <i>)) * (- z5)) * (x *')) + (((- ((1 / 2) * <i>)) * <i>) * (z6 * (x *')))) + (((- ((1 / 2) * <i>)) * (z5 * x)) + ((- ((1 / 2) * <i>)) * ((<i> * z6) * x))) by Th44
.= ((((- ((1 / 2) * <i>)) * (- z5)) * (x *')) + (((- ((1 / 2) * <i>)) * <i>) * (z6 * (x *')))) + ((((- ((1 / 2) * <i>)) * z5) * x) + ((- ((1 / 2) * <i>)) * ((<i> * z6) * x))) by Th44
.= ((((- ((1 / 2) * <i>)) * (- z5)) * (x *')) + (((- ((1 / 2) * <i>)) * <i>) * (z6 * (x *')))) + ((((- ((1 / 2) * <i>)) * z5) * x) + ((- ((1 / 2) * <i>)) * (<i> * (z6 * x)))) by Th44
.= (((1 / 2) * (z6 * x)) + (((- ((1 / 2) * <i>)) * z5) * x)) + (((1 / 2) * (z6 * (x *'))) + ((((1 / 2) * <i>) * z5) * (x *'))) by Th44
.= ((((1 / 2) * (z6 * x)) + (((- ((1 / 2) * <i>)) * z5) * x)) + ((1 / 2) * (z6 * (x *')))) + ((((1 / 2) * <i>) * z5) * (x *')) by A1, A23, A17, A18, A14, A21, Th24
.= ((((1 / 2) * (z6 * x)) + ((1 / 2) * (z6 * (x *')))) + (((- ((1 / 2) * <i>)) * z5) * x)) + ((((1 / 2) * <i>) * z5) * (x *')) by A1, A23, A17, A20, A18, Th24
.= (((1 / 2) * (z6 * x)) + ((1 / 2) * (z6 * (x *')))) + ((((- ((1 / 2) * <i>)) * z5) * x) + ((((1 / 2) * <i>) * z5) * (x *'))) by A1, A23, A17, A20, A14, A19, Th24
.= ((((1 / 2) * z6) * x) + ((1 / 2) * (z6 * (x *')))) + ((((- ((1 / 2) * <i>)) * z5) * x) + ((((1 / 2) * <i>) * z5) * (x *'))) by Th44
.= ((((1 / 2) * z6) * x) + (((1 / 2) * z6) * (x *'))) + ((((- ((1 / 2) * <i>)) * z5) * x) + ((- ((- ((1 / 2) * <i>)) * z5)) * (x *'))) by Th44
.= ((Im a) * (Re x)) + ((Re a) * (Im x)) by ;
hence ( Re (a * x) = ((Re a) * (Re x)) - ((Im a) * (Im x)) & Im (a * x) = ((Im a) * (Re x)) + ((Re a) * (Im x)) ) by A13; :: thesis: verum