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;
A3: now :: thesis: for i being Nat st 1 <= i & i <= len ((a * x) *') holds
((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;
len ((a * x) *') = len (a * x) by Def1;
hence (a * x) *' = (a *') * (x *') by A1, A3, Th3; :: thesis: verum