for a being Real
for n being Nat
for i being non zero Nat holds ((a,(- a)) Subnomial (n + (2 * i))) . (2 * i) = - (a |^ (n + (2 * i)))