let a, b be positive Real; :: thesis: for n being non zero Nat holds Sum (((a + b),0) Subnomial (n + 1)) > Sum ((a,b) Subnomial (n + 1))
let n be non zero Nat; :: thesis: Sum (((a + b),0) Subnomial (n + 1)) > Sum ((a,b) Subnomial (n + 1))
((a + b) - 0) * (Sum (((a + b),0) Subnomial (n + 1))) = ((a + b) |^ ((n + 1) + 1)) - (0 |^ ((n + 1) + 1)) by SumS;
then (a + b) * (Sum (((a + b),0) Subnomial (n + 1))) = (a + b) * ((a + b) |^ (n + 1)) by NEWTON:6;
then Sum (((a + b),0) Subnomial (n + 1)) = (a + b) |^ (n + 1) by XCMPLX_1:5;
then Sum (((a + b),0) Subnomial (n + 1)) = Sum ((a,b) In_Power (n + 1)) by NEWTON:30;
hence Sum (((a + b),0) Subnomial (n + 1)) > Sum ((a,b) Subnomial (n + 1)) by SSI; :: thesis: verum