theorem Th17: :: POLYNOM3:18

for p being natural-valued FinSequence
for i, j being Nat st i <= j holds
Sum (p | i) <= Sum (p | j)