theorem SAA: :: NEWTON04:65
for a being Real
for n being Nat holds Sum ((a,a) Subnomial n) = (n + 1) * (a |^ n)