let a, b be positive Real; 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; 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; verum