let Rseq1, Rseq2 be Real_Sequence; :: thesis: for X being RealUnitarySpace
for seq being sequence of X holds (Rseq1 (#) Rseq2) * seq = Rseq1 * (Rseq2 * seq)
let X be RealUnitarySpace; :: thesis: for seq being sequence of X holds (Rseq1 (#) Rseq2) * seq = Rseq1 * (Rseq2 * seq)
let seq be sequence of X; :: thesis: (Rseq1 (#) Rseq2) * seq = Rseq1 * (Rseq2 * seq)

now

let n be Element of NAT ; :: thesis: ((Rseq1 (#) Rseq2) * seq) . n = (Rseq1 * (Rseq2 * seq)) . n
thus ((Rseq1 (#) Rseq2) * seq) . n = ((Rseq1 (#) Rseq2) . n) * (seq . n) by Def9
.= ((Rseq1 . n) * (Rseq2 . n)) * (seq . n) by SEQ_1:12
.= (Rseq1 . n) * ((Rseq2 . n) * (seq . n)) by RLVECT_1:def 10
.= (Rseq1 . n) * ((Rseq2 * seq) . n) by Def9
.= (Rseq1 * (Rseq2 * seq)) . n by Def9 ; :: thesis: verum

end;

hence (Rseq1 (#) Rseq2) * seq = Rseq1 * (Rseq2 * seq) by FUNCT_2:113; :: thesis: verum