theorem Th5: :: RFUNCT_2:5

for seq being Real_Sequence
for Ns being V43() sequence of NAT holds (seq * Ns) " = (seq ") * Ns