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;
A1: len (a * x) = len x by Th3;
A2: len ((a * x) *' ) = len (a * x) by Def1;
len ((a *' ) * (x *' )) = len (x *' ) by Th3;
then len ((a *' ) * (x *' )) = len x by Def1;
then A3: len ((a * x) *' ) = len ((a *' ) * (x *' )) by A2, Th3;

now

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

end;

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