let i, n be Nat; :: thesis: for a, b being non negative Real holds ((a,b) In_Power n) . i >= ((a,b) Subnomial n) . i
let a, b be non negative Real; :: thesis: ((a,b) In_Power n) . i >= ((a,b) Subnomial n) . i

per cases ( i in dom (Newton_Coeff n) or not i in dom (Newton_Coeff n) ) ;

suppose i in dom (Newton_Coeff n) ; :: thesis: ((a,b) In_Power n) . i >= ((a,b) Subnomial n) . i

then (Newton_Coeff n) . i <> 0 by D1;
then ((Newton_Coeff n) . i) * (((a,b) Subnomial n) . i) >= 1 * (((a,b) Subnomial n) . i) by NAT_1:14, XREAL_1:64;
then ((Newton_Coeff n) (#) ((a,b) Subnomial n)) . i >= ((a,b) Subnomial n) . i by VALUED_1:5;
hence ((a,b) In_Power n) . i >= ((a,b) Subnomial n) . i by INS; :: thesis: verum

end;

suppose not i in dom (Newton_Coeff n) ; :: thesis: ((a,b) In_Power n) . i >= ((a,b) Subnomial n) . i

then not i in (dom ((a,b) In_Power n)) /\ (dom (Newton_Coeff n)) ;
then not i in dom ((a,b) Subnomial n) by VALUED_1:16;
hence ((a,b) In_Power n) . i >= ((a,b) Subnomial n) . i by FUNCT_1:def 2; :: thesis: verum

end;

end;