theorem SSI: :: NEWTON04:87

for a, b being positive Real
for n being non zero Nat holds Sum ((a,b) Subnomial (n + 1)) < Sum ((a,b) In_Power (n + 1))