theorem Th44: :: SEQ_1:46
for r being Real
for seq being Real_Sequence holds (r (#) seq) " = (r ") (#) (seq ")