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