let a be Real; for n being Nat
for i being odd Nat holds ((a,(- a)) Subnomial (n + i)) . i = a |^ (n + i)
let n be Nat; for i being odd Nat holds ((a,(- a)) Subnomial (n + i)) . i = a |^ (n + i)
let i be odd Nat; ((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)
; verum