for seq being Complex_Sequence holds |.seq.| = |.(seq *').| by Lm18;