for r being Complex
for seq being Complex_Sequence holds |.(r (#) seq).| = |.r.| (#) |.seq.|