A1: for i being Nat st i in dom ((a,b) Subnomial n) holds
0 <= ((a,b) Subnomial n) . i
proof
let i be Nat; :: thesis: ( i in dom ((a,b) Subnomial n) implies 0 <= ((a,b) Subnomial n) . i )
assume B1: i in dom ((a,b) Subnomial n) ; :: thesis: 0 <= ((a,b) Subnomial n) . i
B2: ( 1 <= i & i <= len ((a,b) Subnomial ((n + 1) - 1)) ) by B1, FINSEQ_3:25;
then reconsider s = (n + 1) - i as Element of NAT by NAT_1:21;
reconsider l = i - 1 as Nat by B2;
((a,b) Subnomial (l + s)) . (l + 1) > 0 ;
hence 0 <= ((a,b) Subnomial n) . i ; :: thesis: verum
end;
len ((a,b) Subnomial ((n + 1) - 1)) >= 1 by NAT_1:14;
then ( 1 in dom ((a,b) Subnomial ((n + 1) - 1)) & 0 < ((a,b) Subnomial (0 + n)) . (0 + 1) ) by FINSEQ_3:25;
hence Sum ((a,b) Subnomial n) is positive by A1, RVSUM_1:85; :: thesis: verum