theorem ES: :: NEWTON04:66

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