for seq being Complex_Sequence holds
( seq is bounded iff |.seq.| is bounded ) by Lm8, Lm9;