for r being Complex
for seq being Complex_Sequence holds (r (#) seq) " = (r ") (#) (seq ")