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