let a be Real; :: thesis: for n being non zero Nat holds a |^ n = Sum ((a,0) Subnomial n)
let n be non zero Nat; :: thesis: a |^ n = Sum ((a,0) Subnomial n)

per cases ( a is zero or not a is zero ) ;

suppose a is zero ; :: thesis: a |^ n = Sum ((a,0) Subnomial n)

hence a |^ n = Sum ((a,0) Subnomial n) ; :: thesis: verum

end;

suppose A2: not a is zero ; :: thesis: a |^ n = Sum ((a,0) Subnomial n)

(a |^ (n + 1)) - (0 |^ (n + 1)) = (a - 0) * (Sum ((a,0) Subnomial n)) by SumS;
then a * (a |^ n) = a * (Sum ((a,0) Subnomial n)) by NEWTON:6;
hence a |^ n = Sum ((a,0) Subnomial n) by A2, XCMPLX_1:5; :: thesis: verum

end;

end;