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;

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) )
;

end;

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;thus (a * x) . i = a * 0 by A1, FUNCT_1:def 2

.= a * (x . i) by A2, FUNCT_1:def 2 ; :: thesis: verum

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