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

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

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

per cases ( n = 0 or n > 0 ) ;

suppose B1: n = 0 ; :: thesis: Sum ((a,(- a)) Subnomial n) = a |^ n

Sum ((a,(- a)) Subnomial n) = (0 + 1) * (a |^ n) by A1, B1, SAA;
hence Sum ((a,(- a)) Subnomial n) = a |^ n ; :: thesis: verum

end;

suppose B1: n > 0 ; :: thesis: Sum ((a,(- a)) Subnomial n) = a |^ n

(a,(- a)) Subnomial n = (len ((0,0) Subnomial ((n + 1) - 1))) |-> 0 by B1, A1;
hence Sum ((a,(- a)) Subnomial n) = a |^ n by A1, B1, NAT_1:14, NEWTON:11; :: thesis: verum

end;

end;

end;

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

(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
.= 2 * (a |^ (n + 1))
.= 2 * (a * (a |^ n)) by NEWTON:6
.= (2 * a) * (a |^ n) ;
hence Sum ((a,(- a)) Subnomial n) = a |^ n by A1, XCMPLX_1:5; :: thesis: verum

end;

end;