theorem :: COMSEQ_1:32

for seq, seq1, seq9, seq19 being Complex_Sequence holds (seq9 /" seq) (#) (seq19 /" seq1) = (seq9 (#) seq19) /" (seq (#) seq1)