theorem Th5: :: CFCONT_1:5
for seq being Complex_Sequence
for Ns being increasing sequence of NAT holds (seq * Ns) " = (seq ") * Ns