theorem :: CSSPACE2:14

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