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)
let n be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: K64(((Rseq1 (#) Rseq2) * seq),n) = K64((Rseq1 * (Rseq2 * seq)),n)
thus ((Rseq1 (#) Rseq2) * seq) . n = ((Rseq1 (#) Rseq2) . n) * (seq . n) by Def7
.= ((Rseq1 . n) * (Rseq2 . n)) * (seq . n) by SEQ_1:8
.= (Rseq1 . n) * ((Rseq2 . n) * (seq . n)) by RLVECT_1:def 7
.= (Rseq1 . n) * ((Rseq2 * seq) . n) by Def7
.= (Rseq1 * (Rseq2 * seq)) . n by Def7 ; :: thesis: verum