:: deftheorem Def3 defines LagPoly NUMBER19:def 3 :
for F being Field
for x, y being FinSequence of the carrier of F
for b₄ being Polynomial of F holds
( b₄ = LagPoly (x,y) iff ex L being FinSequence of the carrier of (Polynom-Ring F) st
( b₄ = Sum L & len L = len x & ( for i being Nat st 1 <= i & i <= len x holds
L . i = (y /. i) * (LagBPoly (((rng x) \ {(x /. i)}),(x /. i))) ) ) );