A1: ( 1 + 0 <= 1 + i & (i + 1) + 0 <= (i + 1) + n ) by XREAL_1:6;
len ((1,1) Subnomial (((n + i) + 1) - 1)) = (n + i) + 1 ;
then i + 1 in dom ((1,1) Subnomial (n + i)) by A1, FINSEQ_3:25;
then ((1,1) Subnomial (n + i)) . (i + 1) = 1 |^ (n + i) by CONST;
hence ((1,1) Subnomial (n + i)) . (i + 1) = 1 ; :: thesis: verum