let x be FinSequence of COMPLEX ; :: thesis: for a being Complex holds (a * x) *' = (a *') * (x *')

let a be Complex; :: 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;

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

let a be Complex; :: 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 :: thesis: for i being Nat st 1 <= i & i <= len ((a * x) *') holds

((a * x) *') . i = ((a *') * (x *')) . i

len ((a * x) *') = len (a * x)
by Def1;((a * x) *') . i = ((a *') * (x *')) . i

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 Th12

.= (aa *') * ((x . i) *') by COMPLEX1:35

.= (a *') * ((x *') . i) by A2, A4, A6, Def1

.= ((a *') * (x *')) . i by Th12 ;

:: thesis: verum

end;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 Th12

.= (aa *') * ((x . i) *') by COMPLEX1:35

.= (a *') * ((x *') . i) by A2, A4, A6, Def1

.= ((a *') * (x *')) . i by Th12 ;

:: thesis: verum

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