let w be real-valued FinSequence; :: thesis: for r being Real
for i being Nat st i in dom w holds
w +* (i,r) = ((w | (i -' 1)) ^ <*r*>) ^ (w /^ i)
let r be Real; :: thesis: for i being Nat st i in dom w holds
w +* (i,r) = ((w | (i -' 1)) ^ <*r*>) ^ (w /^ i)
let i be Nat; :: thesis: ( i in dom w implies w +* (i,r) = ((w | (i -' 1)) ^ <*r*>) ^ (w /^ i) )
reconsider ww = w as FinSequence of REAL by RVSUM_1:145;
reconsider rr = r as Element of REAL by XREAL_0:def 1;
assume i in dom w ; :: thesis: w +* (i,r) = ((w | (i -' 1)) ^ <*r*>) ^ (w /^ i)
then ww +* (i,rr) = ((ww | (i -' 1)) ^ <*rr*>) ^ (ww /^ i) by FUNCT_7:98;
hence w +* (i,r) = ((w | (i -' 1)) ^ <*r*>) ^ (w /^ i) ; :: thesis: verum