let a be Real; :: thesis: for n being Nat holds a |^ (n + 1) = ((Sum ((a,1) Subnomial n)) * (a - 1)) + 1
let n be Nat; :: thesis: a |^ (n + 1) = ((Sum ((a,1) Subnomial n)) * (a - 1)) + 1
(a |^ (n + 1)) - (1 |^ (n + 1)) = (a - 1) * (Sum ((a,1) Subnomial n)) by SumS;
hence a |^ (n + 1) = ((Sum ((a,1) Subnomial n)) * (a - 1)) + 1 ; :: thesis: verum