theorem Th57: :: NUMBER19:57

for F being Field
for x, y being FinSequence of the carrier of F
for i being Nat holds
( ( y /. i <> 0. F implies Roots ((y /. i) * (LagBPoly (((rng x) \ {(x /. i)}),(x /. i)))) = (rng x) \ {(x /. i)} ) & eval (((y /. i) * (LagBPoly (((rng x) \ {(x /. i)}),(x /. i)))),(x /. i)) = y /. i & ( i in dom x & y /. i <> 0. F implies deg ((y /. i) * (LagBPoly (((rng x) \ {(x /. i)}),(x /. i)))) = (card (rng x)) - 1 ) )