let x be FinSequence of COMPLEX ; :: thesis: for i being Nat
for a being complex number holds (a * x) . i = a * (x . i)
let i be Nat; :: thesis: for a being complex number holds (a * x) . i = a * (x . i)
let a be complex number ; :: 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 Th15;
thus (a * x) . i = a * 0 by A1, FUNCT_1:def 4
.= a * (x . i) by A2, FUNCT_1:def 4 ; :: 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:21;
thus (a * x) . i = (multcomplex [;] aa,(id COMPLEX )) . (x . i) by A3, A4, FUNCT_1:22
.= multcomplex . a,((id COMPLEX ) . (x . i)) by A5, FUNCOP_1:42
.= multcomplex . aa,(x . i) by FUNCT_1:35
.= a * (x . i) by BINOP_2:def 5 ; :: thesis: verum

end;

end;