let i, n be Nat; :: thesis: (Newton_Coeff n) . (i + 1) = n choose i

per cases ( i + 1 in dom (Newton_Coeff n) or not i + 1 in dom (Newton_Coeff n) ) ;

suppose B1: i + 1 in dom (Newton_Coeff n) ; :: thesis: (Newton_Coeff n) . (i + 1) = n choose i

then ( 1 <= i + 1 & i + 1 <= len (Newton_Coeff n) ) by FINSEQ_3:25;
then ( 1 <= i + 1 & i + 1 <= n + 1 ) by NEWTON:def 5;
then reconsider k = (n + 1) - (i + 1) as Element of NAT by NAT_1:21;
( n = i + k & i = (i + 1) - 1 ) ;
hence (Newton_Coeff n) . (i + 1) = n choose i by B1, NEWTON:def 5; :: thesis: verum

end;

suppose B1: not i + 1 in dom (Newton_Coeff n) ; :: thesis: (Newton_Coeff n) . (i + 1) = n choose i

then ( not 1 <= i + 1 or not i + 1 <= len (Newton_Coeff n) ) by FINSEQ_3:25;
then ( not 0 + 1 <= i + 1 or not i + 1 <= n + 1 ) by NEWTON:def 5;
then ( not 0 <= i or not i <= n ) by XREAL_1:6;
then n choose i = 0 by NEWTON:def 3;
hence (Newton_Coeff n) . (i + 1) = n choose i by B1, FUNCT_1:def 2; :: thesis: verum

end;

end;