theorem Th46: :: BHSP_4:46

for a being Real
for Rseq being Real_Sequence
for X being RealUnitarySpace
for seq being sequence of X holds (a (#) Rseq) * seq = a * (Rseq * seq)