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