let F be Field; :: thesis: for x, y being FinSequence of the carrier of F st x is one-to-one holds
for i being Nat st i in dom x holds
eval ((LagPoly (x,y)),(x /. i)) = y /. i
let x, y be FinSequence of the carrier of F; :: thesis: ( x is one-to-one implies for i being Nat st i in dom x holds
eval ((LagPoly (x,y)),(x /. i)) = y /. i )
assume A1: x is one-to-one ; :: thesis: for i being Nat st i in dom x holds
eval ((LagPoly (x,y)),(x /. i)) = y /. i
let i be Nat; :: thesis: ( i in dom x implies eval ((LagPoly (x,y)),(x /. i)) = y /. i )
assume A2: i in dom x ; :: thesis: eval ((LagPoly (x,y)),(x /. i)) = y /. i
consider L being FinSequence of the carrier of (Polynom-Ring F) such that
A3: ( LagPoly (x,y) = Sum L & len L = len x ) and
A4: 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
A5: ( Sum L = f . (len L) & f . 0 = 0. (Polynom-Ring F) ) and
A6: 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;
A7: ( 1 <= i & i <= len x ) by A2, FINSEQ_3:25;
A8: ( x /. i = x . i & x . i in rng x ) by A2, PARTFUN1:def 6, FUNCT_1:def 3;
A9: for n being Nat st n + 1 <= len x & n + 1 <> i holds
eval ((~ (f . n)),(x /. i)) = eval ((~ (f . (n + 1))),(x /. i))
proof
let n be Nat; :: thesis: ( n + 1 <= len x & n + 1 <> i implies eval ((~ (f . n)),(x /. i)) = eval ((~ (f . (n + 1))),(x /. i)) )
set n1 = n + 1;
assume A10: ( n + 1 <= len x & n + 1 <> i ) ; :: thesis: eval ((~ (f . n)),(x /. i)) = eval ((~ (f . (n + 1))),(x /. i))
then A11: ( n + 1 in dom L & n + 1 in dom x ) by NAT_1:11, A3, FINSEQ_3:25;
then A12: ( L . (n + 1) = L /. (n + 1) & x . (n + 1) = x /. (n + 1) ) by PARTFUN1:def 6;
then f . (n + 1) = (f . n) + (L /. (n + 1)) by A10, NAT_1:13, A3, A6;
then ~ (f . (n + 1)) = (~ (f . n)) + (~ (L /. (n + 1))) by POLYNOM3:def 10;
then A13: eval ((~ (f . (n + 1))),(x /. i)) = (eval ((~ (f . n)),(x /. i))) + (eval ((~ (L /. (n + 1))),(x /. i))) by POLYNOM4:19;
A14: L . (n + 1) = (y /. (n + 1)) * (LagBPoly (((rng x) \ {(x /. (n + 1))}),(x /. (n + 1)))) by NAT_1:11, A10, A4;
eval ((~ (L /. (n + 1))),(x /. i)) = 0. F
proof
per cases ( y /. (n + 1) <> 0. F or y /. (n + 1) = 0. F ) ;
suppose y /. (n + 1) <> 0. F ; :: thesis: eval ((~ (L /. (n + 1))),(x /. i)) = 0. F
then A15: Roots (~ (L /. (n + 1))) = (rng x) \ {(x /. (n + 1))} by Th57, A14, A12;
x /. i in (rng x) \ {(x /. (n + 1))} by ZFMISC_1:56, A10, FUNCT_1:def 4, A1, A2, A11, A8, A12;
then x /. i is_a_root_of ~ (L /. (n + 1)) by A15, POLYNOM5:def 10;
hence eval ((~ (L /. (n + 1))),(x /. i)) = 0. F by POLYNOM5:def 7; :: thesis: verum
end;
suppose y /. (n + 1) = 0. F ; :: thesis: eval ((~ (L /. (n + 1))),(x /. i)) = 0. F
then L /. (n + 1) = 0_. F by A14, A12, RING_4:8;
hence eval ((~ (L /. (n + 1))),(x /. i)) = 0. F by POLYNOM4:17; :: thesis: verum
end;
end;
end;
hence eval ((~ (f . n)),(x /. i)) = eval ((~ (f . (n + 1))),(x /. i)) by A13; :: thesis: verum
end;
defpred S1[ Nat] means ( $1 < i implies eval ((~ (f . $1)),(x /. i)) = 0. F );
0. (Polynom-Ring F) = 0_. F by POLYNOM3:def 10;
then A16: S1[ 0 ] by A5, POLYNOM4:17;
A17: for n being Nat st S1[n] holds
S1[n + 1] by A9, A7, NAT_1:13, XXREAL_0:2;
A18: for n being Nat holds S1[n] from NAT_1:sch 2(A16, A17);
 defpred S2[ Nat] means ( i <= $1 & $1 <= len x implies eval ((~ (f . $1)),(x /. i)) = y /. i );
A19: S2[ 0 ] by A2, FINSEQ_3:25;
A20: for n being Nat st S2[n] holds
S2[n + 1]
proof
let n be Nat; :: thesis: ( S2[n] implies S2[n + 1] )
assume A21: S2[n] ; :: thesis: S2[n + 1]
set n1 = n + 1;
assume A22: ( i <= n + 1 & n + 1 <= len x ) ; :: thesis: eval ((~ (f . (n + 1))),(x /. i)) = y /. i
per cases then ( i = n + 1 or i < n + 1 ) by XXREAL_0:1;
suppose A23: i = n + 1 ; :: thesis: eval ((~ (f . (n + 1))),(x /. i)) = y /. i
then n < i by NAT_1:13;
then A24: eval ((~ (f . n)),(x /. i)) = 0. F by A18;
( n + 1 in dom L & n + 1 in dom x ) by NAT_1:11, A3, A22, FINSEQ_3:25;
then A25: ( L . (n + 1) = L /. (n + 1) & x . (n + 1) = x /. (n + 1) ) by PARTFUN1:def 6;
then f . (n + 1) = (f . n) + (L /. (n + 1)) by A22, NAT_1:13, A3, A6;
then ~ (f . (n + 1)) = (~ (f . n)) + (~ (L /. (n + 1))) by POLYNOM3:def 10;
then A26: eval ((~ (f . (n + 1))),(x /. i)) = (eval ((~ (f . n)),(x /. i))) + (eval ((~ (L /. (n + 1))),(x /. i))) by POLYNOM4:19;
L . (n + 1) = (y /. i) * (LagBPoly (((rng x) \ {(x /. i)}),(x /. i))) by A22, NAT_1:11, A23, A4;
hence eval ((~ (f . (n + 1))),(x /. i)) = y /. i by A26, A24, A25, Th57; :: thesis: verum
end;
suppose i < n + 1 ; :: thesis: eval ((~ (f . (n + 1))),(x /. i)) = y /. i
hence eval ((~ (f . (n + 1))),(x /. i)) = y /. i by A21, A22, A9, NAT_1:13; :: thesis: verum
end;
end;
end;
for n being Nat holds S2[n] from NAT_1:sch 2(A19, A20);
 then eval ((~ (f . (len x))),(x /. i)) = y /. i by A7;
hence eval ((LagPoly (x,y)),(x /. i)) = y /. i by A3, A5; :: thesis: verum