theorem lem24: :: REALALG3:14

for F being Field
for f being FinSequence of the carrier of (Polynom-Ring F)
for p being non zero Polynomial of F st p = Sum f holds
for g being FinSequence of F
for n being Nat st ( for i being Element of dom f
for q being Polynomial of F st q = f . i holds
deg q <= n ) holds
deg p <= n