theorem Th14: :: HILB10_8:14

for a, b, c, d being Nat st a <= b & b <= c & 2 * c <= d & c > 0 holds
for f being FinSequence of REAL st len f = (b - a) + 1 & ( for i being Nat st i + 1 in dom f holds
f . (i + 1) = (c choose (a + i)) * (d |^ (c -' (a + i))) ) holds
( 0 < Sum f & Sum f < (2 * (c |^ a)) * (d |^ (c -' a)) )