theorem Th16: :: TOPRNS_1:16

for N being Nat
for seq being Real_Sequence of N holds 1 * seq = seq