theorem SumS: :: NEWTON04:51

for a, b being Real
for n being Nat holds (a |^ (n + 1)) - (b |^ (n + 1)) = (a - b) * (Sum ((a,b) Subnomial n))