set f = (a,b) Subnomial n;
let e be Nat; :: according to RVSUM_3:def 1 :: thesis: ( not e in dom ((a,b) Subnomial n) or not ((a,b) Subnomial n) . e <= 0 )
assume A1: e in dom ((a,b) Subnomial n) ; :: thesis: not ((a,b) Subnomial n) . e <= 0
then 1 <= e by FINSEQ_3:25;
then reconsider m = e - 1 as Element of NAT by INT_1:3;
A2: e <= len ((a,b) Subnomial n) by A1, FINSEQ_3:25;
(len ((a,b) Subnomial n)) - 1 = (n + 1) - 1 ;
then reconsider k = n - m as Element of NAT by A2, XREAL_1:7, INT_1:5;
((a,b) Subnomial n) . e = (a |^ k) * (b |^ m) by A1, NEWTON04:def 2;
hence ((a,b) Subnomial n) . e > 0 ; :: thesis: verum