theorem :: NEWTON04:53

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