let x be FinSequence of COMPLEX ; :: thesis: for a being complex number holds (a * x) *' = (a *' ) * (x *' )
let a be complex number ; :: thesis: (a * x) *' = (a *' ) * (x *' )
reconsider aa = a as Element of COMPLEX by XCMPLX_0:def 2;
len ((a *' ) * (x *' )) = len (x *' ) by Th3;
then A1: len ((a *' ) * (x *' )) = len x by Def1;
A2: len (a * x) = len x by Th3;

A3: now

let i be Nat; :: thesis: ( 1 <= i & i <= len ((a * x) *' ) implies ((a * x) *' ) . i = ((a *' ) * (x *' )) . i )
assume that
A4: 1 <= i and
A5: i <= len ((a * x) *' ) ; :: thesis: ((a * x) *' ) . i = ((a *' ) * (x *' )) . i
A6: i <= len (a * x) by A5, Def1;
hence ((a * x) *' ) . i = ((a * x) . i) *' by A4, Def1
.= (aa * (x . i)) *' by Th16
.= (aa *' ) * ((x . i) *' ) by COMPLEX1:121
.= (a *' ) * ((x *' ) . i) by A2, A4, A6, Def1
.= ((a *' ) * (x *' )) . i by Th16 ;
:: thesis: verum

end;

len ((a * x) *' ) = len (a * x) by Def1;
hence (a * x) *' = (a *' ) * (x *' ) by A1, A3, Th3, FINSEQ_1:18; :: thesis: verum