theorem Th54: :: NUMBER19:54

for F being Field
for X being finite Subset of F
for x being Element of F st not x in X holds
( Roots (LagBPoly (X,x)) = X & eval ((LagBPoly (X,x)),x) = 1. F & deg (LagBPoly (X,x)) = card X )