theorem Th45: :: COMSEQ_1:46

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