A1: len ((1,(- 1)) Subnomial ((((2 * i) + n) + 1) - 1)) = ((2 * i) + n) + 1 ;
( i + i >= 1 + 0 & (2 * i) + (n + 1) >= (2 * i) + 0 ) by XREAL_1:6, NAT_1:14;
then A2: 2 * i in dom ((1,(- 1)) Subnomial ((2 * i) + n)) by A1, FINSEQ_3:25;
reconsider k = (2 * i) - 1 as odd Nat ;
n + 1 = ((2 * i) + n) - k ;
then ((1,(- 1)) Subnomial (n + (2 * i))) . (2 * i) = (1 |^ (n + 1)) * ((- 1) |^ k) by A2, Def2
.= 1 * (- 1) ;
hence ((1,(- 1)) Subnomial ((2 * i) + n)) . (2 * i) = - 1 ; :: thesis: verum