let F be Field; :: thesis: for x, y being FinSequence of the carrier of F holds degree (LagPoly (x,y)) <= (len x) - 1
let x, y be FinSequence of the carrier of F; :: thesis: degree (LagPoly (x,y)) <= (len x) - 1
consider L being FinSequence of the carrier of (Polynom-Ring F) such that
A1: ( LagPoly (x,y) = Sum L & len L = len x ) and
A2: for i being Nat st 1 <= i & i <= len x holds
L . i = (y /. i) * (LagBPoly (((rng x) \ {(x /. i)}),(x /. i))) by Def3;
consider f being sequence of (Polynom-Ring F) such that
A3: ( Sum L = f . (len L) & f . 0 = 0. (Polynom-Ring F) ) and
A4: for j being Nat
for v being Element of (Polynom-Ring F) st j < len L & v = L . (j + 1) holds
f . (j + 1) = (f . j) + v by RLVECT_1:def 12;
defpred S₁[ Nat] means ( $1 <= len L implies deg (~ (f . $1)) <= (len x) - 1 );
~ (f . 0) = 0_. F by A3, POLYNOM3:def 10;
then ( deg (~ (f . 0)) = 0 - 1 & 0 - 1 <= (len x) - 1 ) by XREAL_1:9, HURWITZ:20;
then A5: S₁[ 0 ] ;
A6: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A7: S₁[n] ; :: thesis: S₁[n + 1]
set n1 = n + 1;
assume A8: n + 1 <= len L ; :: thesis: deg (~ (f . (n + 1))) <= (len x) - 1
A9: ( n + 1 in dom L & n + 1 in dom x ) by A8, A1, NAT_1:11, FINSEQ_3:25;
then A10: L . (n + 1) = L /. (n + 1) by PARTFUN1:def 6;
then f . (n + 1) = (f . n) + (L /. (n + 1)) by A8, NAT_1:13, A4;
then ~ (f . (n + 1)) = (~ (f . n)) + (~ (L /. (n + 1))) by POLYNOM3:def 10;
then A11: deg (~ (f . (n + 1))) <= max ((deg (~ (f . n))),(deg (~ (L /. (n + 1))))) by HURWITZ:22;
A12: L . (n + 1) = (y /. (n + 1)) * (LagBPoly (((rng x) \ {(x /. (n + 1))}),(x /. (n + 1)))) by NAT_1:11, A8, A1, A2;
deg (~ (L /. (n + 1))) <= (len x) - 1

proof

per cases ( y /. (n + 1) <> 0. F or y /. (n + 1) = 0. F ) ;

suppose y /. (n + 1) <> 0. F ; :: thesis: deg (~ (L /. (n + 1))) <= (len x) - 1

then A13: deg (~ (L /. (n + 1))) = (card (rng x)) - 1 by A10, A12, Th57, A9;
dom x = Seg (len x) by FINSEQ_1:def 3;
then ( card (rng x) <= card (dom x) & card (dom x) = len x ) by CARD_2:47;
hence deg (~ (L /. (n + 1))) <= (len x) - 1 by A13, XREAL_1:9; :: thesis: verum

end;

suppose y /. (n + 1) = 0. F ; :: thesis: deg (~ (L /. (n + 1))) <= (len x) - 1

then L /. (n + 1) = 0_. F by A12, A10, RING_4:8;
then ( deg (~ (L /. (n + 1))) = 0 - 1 & 0 - 1 <= (len x) - 1 ) by XREAL_1:9, HURWITZ:20;
hence deg (~ (L /. (n + 1))) <= (len x) - 1 ; :: thesis: verum

end;

end;

end;

then max ((deg (~ (f . n))),(deg (~ (L /. (n + 1))))) <= (len x) - 1 by A8, NAT_1:13, A7, XXREAL_0:16;
hence deg (~ (f . (n + 1))) <= (len x) - 1 by A11, XXREAL_0:2; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A5, A6);
then S₁[ len L] ;
hence degree (LagPoly (x,y)) <= (len x) - 1 by A1, A3; :: thesis: verum