theorem :: NUMBER19:62

for F being Field
for z being FinSequence of the carrier of F
for i being Nat st i in dom z & z is one-to-one holds
LagBPoly (((rng z) \ {(z . i)}),(z /. i)) = ((eval ((LagIPoly (z,i)),(z /. i))) ") * (LagIPoly (z,i))