let X be ComplexUnitarySpace; :: thesis: for seq being sequence of X
for Cseq1, Cseq2 being Complex_Sequence holds (Cseq1 (#) Cseq2) * seq = Cseq1 * (Cseq2 * seq)
let seq be sequence of X; :: thesis: for Cseq1, Cseq2 being Complex_Sequence holds (Cseq1 (#) Cseq2) * seq = Cseq1 * (Cseq2 * seq)
let Cseq1, Cseq2 be Complex_Sequence; :: thesis: (Cseq1 (#) Cseq2) * seq = Cseq1 * (Cseq2 * seq)

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

let n be Element of NAT ; :: thesis: ((Cseq1 (#) Cseq2) * seq) . n = (Cseq1 * (Cseq2 * seq)) . n
thus ((Cseq1 (#) Cseq2) * seq) . n = ((Cseq1 (#) Cseq2) . n) * (seq . n) by Def8
.= ((Cseq1 . n) * (Cseq2 . n)) * (seq . n) by VALUED_1:5
.= (Cseq1 . n) * ((Cseq2 . n) * (seq . n)) by CLVECT_1:def 4
.= (Cseq1 . n) * ((Cseq2 * seq) . n) by Def8
.= (Cseq1 * (Cseq2 * seq)) . n by Def8 ; :: thesis: verum

end;

hence (Cseq1 (#) Cseq2) * seq = Cseq1 * (Cseq2 * seq) by FUNCT_2:63; :: thesis: verum