theorem CopyForValued: :: RVSUM_3:23

for w being real-valued FinSequence
for r being Real
for i being Nat st i in dom w holds
w +* (i,r) = ((w | (i -' 1)) ^ <*r*>) ^ (w /^ i)