theorem :: COMSEQ_1:49

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