let p be FinSequence of REAL ; :: thesis: for i being Element of NAT st i < len p holds
Sum (p | (i + 1)) = (Sum (p | i)) + (p . (i + 1))
let i be Element of NAT ; :: thesis: ( i < len p implies Sum (p | (i + 1)) = (Sum (p | i)) + (p . (i + 1)) )
assume i < len p ; :: thesis: Sum (p | (i + 1)) = (Sum (p | i)) + (p . (i + 1))
then p | (i + 1) = (p | i) ^ <*(p . (i + 1))*> by FINSEQ_5:83;
hence Sum (p | (i + 1)) = (Sum (p | i)) + (p . (i + 1)) by RVSUM_1:74; :: thesis: verum