theorem Th5: :: CFCONT_1:5

for seq being Complex_Sequence
for Ns being V42() sequence of NAT holds (seq * Ns) " = (seq ") * Ns