theorem :: NEWTON04:89

for a, b being Real
for n, i being Nat holds ((a,b) Subnomial n) . i <= ((|.a.|,|.b.|) Subnomial n) . i