theorem Th4: :: POLYNOM3:4

for p being natural-valued FinSequence
for i being Nat st i in dom p holds
Sum p >= p . i