let a be Real; :: thesis: for Rseq being Real_Sequence
for X being RealUnitarySpace
for seq being sequence of X holds (a (#) Rseq) * seq = a * (Rseq * seq)
let Rseq be Real_Sequence; :: thesis: for X being RealUnitarySpace
for seq being sequence of X holds (a (#) Rseq) * seq = a * (Rseq * seq)
let X be RealUnitarySpace; :: thesis: for seq being sequence of X holds (a (#) Rseq) * seq = a * (Rseq * seq)
let seq be sequence of X; :: thesis: (a (#) Rseq) * seq = a * (Rseq * seq)

now

let n be Element of NAT ; :: thesis: ((a (#) Rseq) * seq) . n = (a * (Rseq * seq)) . n
thus ((a (#) Rseq) * seq) . n = ((a (#) Rseq) . n) * (seq . n) by Def9
.= (a * (Rseq . n)) * (seq . n) by SEQ_1:13
.= a * ((Rseq . n) * (seq . n)) by RLVECT_1:def 9
.= a * ((Rseq * seq) . n) by Def9
.= (a * (Rseq * seq)) . n by NORMSP_1:def 8 ; :: thesis: verum

end;

hence (a (#) Rseq) * seq = a * (Rseq * seq) by FUNCT_2:113; :: thesis: verum