let p be complex-valued FinSequence; :: thesis: for i being Nat st i < len p holds
Sum (p | (i + 1)) = (Sum (p | i)) + (p . (i + 1))
let i be 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_2:31; :: thesis: verum