A1: len ((1,(- 1)) 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 ((1,(- 1)) Subnomial (i + n)) by A1, FINSEQ_3:25;
reconsider k = i - 1 as even Nat ;
n + 1 = (i + n) - k ;
then ((1,(- 1)) Subnomial (n + i)) . i = (1 |^ (n + 1)) * ((- 1) |^ k) by A2, Def2
.= 1 * 1 ;
hence ((1,(- 1)) Subnomial (n + i)) . i = 1 ; :: thesis: verum