theorem Th23: :: SEQ_1:23

for r, p being Real
for seq being Real_Sequence holds (r * p) (#) seq = r (#) (p (#) seq)