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

suppose a is zero ; :: thesis: Sum ((a,(- a)) Subnomial n) is zero

then (a,(- a)) Subnomial n = (len ((0,0) Subnomial ((n + 1) - 1))) |-> 0 ;
hence Sum ((a,(- a)) Subnomial n) is zero ; :: thesis: verum

end;

suppose not a is zero ; :: thesis: Sum ((a,(- a)) Subnomial n) is zero

then A1: 2 * a <> 0 ;
(a - (- a)) * (Sum ((a,(- a)) Subnomial n)) = (a |^ (n + 1)) - (((- 1) * a) |^ (n + 1)) by SumS
.= (a |^ (n + 1)) - (((- 1) |^ (n + 1)) * (a |^ (n + 1))) by NEWTON:7
.= (a |^ (n + 1)) - (1 * (a |^ (n + 1))) ;
hence Sum ((a,(- a)) Subnomial n) is zero by A1; :: thesis: verum

end;

end;