theorem Th8: :: COMSEQ_1:8

for seq1, seq2, seq3 being Complex_Sequence holds (seq1 (#) seq2) (#) seq3 = seq1 (#) (seq2 (#) seq3)