theorem :: NUMBER19:58

for F being Field
for x, y being FinSequence of the carrier of F holds degree (LagPoly (x,y)) <= (len x) - 1