let F be Field; :: thesis: 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))
let z be FinSequence of the carrier of F; :: thesis: 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))
let i be Nat; :: thesis: ( i in dom z & z is one-to-one implies LagBPoly (((rng z) \ {(z . i)}),(z /. i)) = ((eval ((LagIPoly (z,i)),(z /. i))) ") * (LagIPoly (z,i)) )
assume A1: ( i in dom z & z is one-to-one ) ; :: thesis: LagBPoly (((rng z) \ {(z . i)}),(z /. i)) = ((eval ((LagIPoly (z,i)),(z /. i))) ") * (LagIPoly (z,i))
reconsider D = Del (z,i) as one-to-one FinSequence of the carrier of F by A1, NAT_5:6;
rng D = (rng z) \ {(z . i)} by Th61, A1, FINSEQ_4:4;
hence LagBPoly (((rng z) \ {(z . i)}),(z /. i)) = ((eval ((~ (Product (rpoly (((len D) |-> 1),D)))),(z /. i))) ") * (LagIPoly (z,i)) by Def2
.= ((eval ((LagIPoly (z,i)),(z /. i))) ") * (LagIPoly (z,i)) ;
:: thesis: verum