let a be Real; :: thesis: for n being Nat
for i being non zero Nat holds ((a,(- a)) Subnomial (n + (2 * i))) . (2 * i) = - (a |^ (n + (2 * i)))
let n be Nat; :: thesis: for i being non zero Nat holds ((a,(- a)) Subnomial (n + (2 * i))) . (2 * i) = - (a |^ (n + (2 * i)))
let i be non zero Nat; :: thesis: ((a,(- a)) Subnomial (n + (2 * i))) . (2 * i) = - (a |^ (n + (2 * i)))
A1: ( len ((a,a) Subnomial (((n + (2 * i)) + 1) - 1)) = (n + (2 * i)) + 1 & len ((a,(- a)) Subnomial (((n + (2 * i)) + 1) - 1)) = (n + (2 * i)) + 1 ) ;
( 2 * i >= 1 & (2 * i) + (n + 1) >= (2 * i) + 0 ) by XREAL_1:6, NAT_1:14;
then A2: ( 2 * i in dom ((a,a) Subnomial ((2 * i) + n)) & 2 * i in dom ((a,(- a)) Subnomial ((2 * i) + n)) ) by A1, FINSEQ_3:25;
then (((a * 1),((- 1) * a)) Subnomial (n + (2 * i))) . (2 * i) = (((a,a) Subnomial (n + (2 * i))) . (2 * i)) * (((1,(- 1)) Subnomial (n + (2 * i))) . (2 * i)) by STT
.= (a |^ (n + (2 * i))) * (- 1) by A2, CONST ;
hence ((a,(- a)) Subnomial (n + (2 * i))) . (2 * i) = - (a |^ (n + (2 * i))) ; :: thesis: verum