theorem Th3: :: RFUNCT_2:3

for p being Real
for seq being Real_Sequence
for Ns being increasing sequence of NAT holds (p (#) seq) * Ns = p (#) (seq * Ns)