let a, b be positive Real; :: thesis: for n being non zero Nat holds Sum ((a,b) Subnomial (n + 1)) < Sum ((a,b) In_Power (n + 1))
let n be non zero Nat; :: thesis: Sum ((a,b) Subnomial (n + 1)) < Sum ((a,b) In_Power (n + 1))
A1: for i being Nat holds ((a,b) Subnomial (n + 1)) . i <= ((a,b) In_Power (n + 1)) . i by ILS;
reconsider h = (a,b) Subnomial (n + 1) as nonnegative-yielding FinSequence of REAL ;
reconsider g = (a,b) In_Power (n + 1) as nonnegative-yielding FinSequence of REAL ;
1 + 0 < 1 + n by XREAL_1:6;
then 1 * (((a,b) Subnomial (n + 1)) . (n + 1)) < ((Newton_Coeff (n + 1)) . (n + 1)) * (((a,b) Subnomial (n + 1)) . (n + 1)) by XREAL_1:68;
then ((a,b) Subnomial (n + 1)) . (n + 1) < ((Newton_Coeff (n + 1)) (#) ((a,b) Subnomial (n + 1))) . (n + 1) by VALUED_1:5;
then ((a,b) Subnomial (n + 1)) . (n + 1) < ((a,b) In_Power (n + 1)) . (n + 1) by INS;
hence Sum ((a,b) Subnomial (n + 1)) < Sum ((a,b) In_Power (n + 1)) by A1, NYS1; :: thesis: verum