for seq, seq9 being Complex_Sequence holds |.(seq (#) seq9).| = |.seq.| (#) |.seq9.|