let F be Field; :: thesis: for x, y being FinSequence of the carrier of F
for i being Nat holds
( ( y /. i <> 0. F implies Roots ((y /. i) * (LagBPoly (((rng x) \ {(x /. i)}),(x /. i)))) = (rng x) \ {(x /. i)} ) & eval (((y /. i) * (LagBPoly (((rng x) \ {(x /. i)}),(x /. i)))),(x /. i)) = y /. i & ( i in dom x & y /. i <> 0. F implies deg ((y /. i) * (LagBPoly (((rng x) \ {(x /. i)}),(x /. i)))) = (card (rng x)) - 1 ) )
let x, y be FinSequence of the carrier of F; :: thesis: for i being Nat holds
( ( y /. i <> 0. F implies Roots ((y /. i) * (LagBPoly (((rng x) \ {(x /. i)}),(x /. i)))) = (rng x) \ {(x /. i)} ) & eval (((y /. i) * (LagBPoly (((rng x) \ {(x /. i)}),(x /. i)))),(x /. i)) = y /. i & ( i in dom x & y /. i <> 0. F implies deg ((y /. i) * (LagBPoly (((rng x) \ {(x /. i)}),(x /. i)))) = (card (rng x)) - 1 ) )
let i be Nat; :: thesis: ( ( y /. i <> 0. F implies Roots ((y /. i) * (LagBPoly (((rng x) \ {(x /. i)}),(x /. i)))) = (rng x) \ {(x /. i)} ) & eval (((y /. i) * (LagBPoly (((rng x) \ {(x /. i)}),(x /. i)))),(x /. i)) = y /. i & ( i in dom x & y /. i <> 0. F implies deg ((y /. i) * (LagBPoly (((rng x) \ {(x /. i)}),(x /. i)))) = (card (rng x)) - 1 ) )
set Rx = (rng x) \ {(x /. i)};
x /. i in {(x /. i)} by TARSKI:def 1;
then A1: not x /. i in (rng x) \ {(x /. i)} by XBOOLE_0:def 5;
thus ( y /. i <> 0. F implies Roots ((y /. i) * (LagBPoly (((rng x) \ {(x /. i)}),(x /. i)))) = (rng x) \ {(x /. i)} ) :: thesis: ( eval (((y /. i) * (LagBPoly (((rng x) \ {(x /. i)}),(x /. i)))),(x /. i)) = y /. i & ( i in dom x & y /. i <> 0. F implies deg ((y /. i) * (LagBPoly (((rng x) \ {(x /. i)}),(x /. i)))) = (card (rng x)) - 1 ) )

proof

assume y /. i <> 0. F ; :: thesis: Roots ((y /. i) * (LagBPoly (((rng x) \ {(x /. i)}),(x /. i)))) = (rng x) \ {(x /. i)}
then not y /. i is zero by STRUCT_0:def 12;
then Roots ((y /. i) * (LagBPoly (((rng x) \ {(x /. i)}),(x /. i)))) = Roots (LagBPoly (((rng x) \ {(x /. i)}),(x /. i))) by RING_5:19;
hence Roots ((y /. i) * (LagBPoly (((rng x) \ {(x /. i)}),(x /. i)))) = (rng x) \ {(x /. i)} by A1, Th54; :: thesis: verum

end;

thus eval (((y /. i) * (LagBPoly (((rng x) \ {(x /. i)}),(x /. i)))),(x /. i)) = (y /. i) * (eval ((LagBPoly (((rng x) \ {(x /. i)}),(x /. i))),(x /. i))) by POLYNOM5:30
.= (y /. i) * (1. F) by A1, Th54
.= y /. i ; :: thesis: ( i in dom x & y /. i <> 0. F implies deg ((y /. i) * (LagBPoly (((rng x) \ {(x /. i)}),(x /. i)))) = (card (rng x)) - 1 )
assume A2: ( i in dom x & y /. i <> 0. F ) ; :: thesis: deg ((y /. i) * (LagBPoly (((rng x) \ {(x /. i)}),(x /. i)))) = (card (rng x)) - 1
then not y /. i is zero by STRUCT_0:def 12;
then A3: deg ((y /. i) * (LagBPoly (((rng x) \ {(x /. i)}),(x /. i)))) = deg (LagBPoly (((rng x) \ {(x /. i)}),(x /. i))) by RING_5:4
.= card ((rng x) \ {(x /. i)}) by A1, Th54 ;
( x /. i = x . i & x . i in rng x ) by A2, PARTFUN1:def 6, FUNCT_1:def 3;
then rng x = ((rng x) \ {(x /. i)}) \/ {(x /. i)} by ZFMISC_1:116;
then card (rng x) = (card ((rng x) \ {(x /. i)})) + 1 by A1, CARD_2:41;
hence deg ((y /. i) * (LagBPoly (((rng x) \ {(x /. i)}),(x /. i)))) = (card (rng x)) - 1 by A3; :: thesis: verum