:: deftheorem Def2 defines LagBPoly NUMBER19:def 2 :
for F being Field
for X being finite Subset of F
for x being Element of F
for b₄ being Polynomial of F holds
( b₄ = LagBPoly (X,x) iff for z being one-to-one FinSequence of the carrier of F st rng z = X holds
b₄ = ((eval ((~ (Product (rpoly (((len z) |-> 1),z)))),x)) ") * (~ (Product (rpoly (((len z) |-> 1),z)))) );