let F be Field; :: thesis: 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 )
let X be finite Subset of F; :: thesis: 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 )
let x be Element of F; :: thesis: ( not x in X implies ( Roots (LagBPoly (X,x)) = X & eval ((LagBPoly (X,x)),x) = 1. F & deg (LagBPoly (X,x)) = card X ) )
assume A1: not x in X ; :: thesis: ( Roots (LagBPoly (X,x)) = X & eval ((LagBPoly (X,x)),x) = 1. F & deg (LagBPoly (X,x)) = card X )
A2: rng (canFS X) = X by FUNCT_2:def 3;
then reconsider z = canFS X as one-to-one FinSequence of the carrier of F by FINSEQ_1:def 4;
A3: LagBPoly (X,x) = ((eval ((~ (Product (rpoly (((len z) |-> 1),z)))),x)) ") * (~ (Product (rpoly (((len z) |-> 1),z)))) by A2, Def2;
then A4: eval ((LagBPoly (X,x)),x) = ((eval ((~ (Product (rpoly (((len z) |-> 1),z)))),x)) ") * (eval ((~ (Product (rpoly (((len z) |-> 1),z)))),x)) by RING_5:7;
A5: Roots (~ (Product (rpoly (((len z) |-> 1),z)))) = rng z by Th53;
then not x is_a_root_of ~ (Product (rpoly (((len z) |-> 1),z))) by A1, A2, POLYNOM5:def 10;
then A6: eval ((~ (Product (rpoly (((len z) |-> 1),z)))),x) <> 0. F by POLYNOM5:def 7;
then not (eval ((~ (Product (rpoly (((len z) |-> 1),z)))),x)) " is zero by STRUCT_0:def 12, VECTSP_1:25;
hence ( Roots (LagBPoly (X,x)) = X & eval ((LagBPoly (X,x)),x) = 1. F ) by A5, A2, A6, A4, VECTSP_1:def 10, A3, RING_5:19; :: thesis: deg (LagBPoly (X,x)) = card X
not (eval ((~ (Product (rpoly (((len z) |-> 1),z)))),x)) " is zero by A6, STRUCT_0:def 12, VECTSP_1:25;
then deg (LagBPoly (X,x)) = deg (~ (Product (rpoly (((len z) |-> 1),z)))) by A3, RING_5:4;
then deg (LagBPoly (X,x)) = Sum ((len z) |-> 1) by Th49;
then deg (LagBPoly (X,x)) = (len z) * 1 by RVSUM_1:80;
hence deg (LagBPoly (X,x)) = card X by FINSEQ_1:93; :: thesis: verum