let x be FinSequence of COMPLEX ; :: thesis: for i being Nat
for a being Complex holds (a * x) . i = a * (x . i)
let i be Nat; :: thesis: for a being Complex holds (a * x) . i = a * (x . i)
let a be Complex; :: thesis: (a * x) . i = a * (x . i)
reconsider aa = a as Element of COMPLEX by XCMPLX_0:def 2;

per cases ( not i in dom (a * x) or i in dom (a * x) ) ;

suppose A1: not i in dom (a * x) ; :: thesis: (a * x) . i = a * (x . i)

then A2: not i in dom x by Th11;
thus (a * x) . i = a * 0 by A1, FUNCT_1:def 2
.= a * (x . i) by A2, FUNCT_1:def 2 ; :: thesis: verum

end;

suppose A3: i in dom (a * x) ; :: thesis: (a * x) . i = a * (x . i)

set a9 = x . i;
A4: a * x = (multcomplex [;] (aa,(id COMPLEX))) * x by Lm1;
then A5: x . i in dom (multcomplex [;] (aa,(id COMPLEX))) by A3, FUNCT_1:11;
thus (a * x) . i = (multcomplex [;] (aa,(id COMPLEX))) . (x . i) by A3, A4, FUNCT_1:12
.= multcomplex . (a,((id COMPLEX) . (x . i))) by A5, FUNCOP_1:32
.= a * (x . i) by BINOP_2:def 5 ; :: thesis: verum

end;

end;