for seq1, seq2 being Real_Sequence
for r being Real holds seq1 (##) (r (#) seq2) = r (#) (seq1 (##) seq2)