let X be ComplexUnitarySpace; :: thesis: for seq being sequence of X
for Cseq being Complex_Sequence
for z being Complex holds (z (#) Cseq) * seq = z * (Cseq * seq)
let seq be sequence of X; :: thesis: for Cseq being Complex_Sequence
for z being Complex holds (z (#) Cseq) * seq = z * (Cseq * seq)
let Cseq be Complex_Sequence; :: thesis: for z being Complex holds (z (#) Cseq) * seq = z * (Cseq * seq)
let z be Complex; :: thesis: (z (#) Cseq) * seq = z * (Cseq * seq)

now :: thesis: for n being Element of NAT holds ((z (#) Cseq) * seq) . n = (z * (Cseq * seq)) . n

let n be Element of NAT ; :: thesis: ((z (#) Cseq) * seq) . n = (z * (Cseq * seq)) . n
thus ((z (#) Cseq) * seq) . n = ((z (#) Cseq) . n) * (seq . n) by Def8
.= (z * (Cseq . n)) * (seq . n) by VALUED_1:6
.= z * ((Cseq . n) * (seq . n)) by CLVECT_1:def 4
.= z * ((Cseq * seq) . n) by Def8
.= (z * (Cseq * seq)) . n by CLVECT_1:def 14 ; :: thesis: verum

end;

hence (z (#) Cseq) * seq = z * (Cseq * seq) by FUNCT_2:63; :: thesis: verum