let n be Nat; :: thesis: for i, z being FinSequence of the carrier of F_Rat st i = idseq n & z = primesFinS n holds
for k being Nat st k < n holds
eval ((LagPoly (i,z)),(In ((k + 1),F_Rat))) = primenumber k
let i, z be FinSequence of the carrier of F_Rat; :: thesis: ( i = idseq n & z = primesFinS n implies for k being Nat st k < n holds
eval ((LagPoly (i,z)),(In ((k + 1),F_Rat))) = primenumber k )
assume A1: ( i = idseq n & z = primesFinS n ) ; :: thesis: for k being Nat st k < n holds
eval ((LagPoly (i,z)),(In ((k + 1),F_Rat))) = primenumber k
let k be Nat; :: thesis: ( k < n implies eval ((LagPoly (i,z)),(In ((k + 1),F_Rat))) = primenumber k )
assume A2: k < n ; :: thesis: eval ((LagPoly (i,z)),(In ((k + 1),F_Rat))) = primenumber k
A3: i is one-to-one by A1, FINSEQ_2:55;
A4: n = len i by A1;
A5: ( 1 <= k + 1 & k + 1 <= n ) by A2, NAT_1:11, NAT_1:13;
then A6: ( k + 1 in dom i & k + 1 in Seg n ) by A4, FINSEQ_3:25;
then A7: i /. (k + 1) = i . (k + 1) by PARTFUN1:def 6
.= k + 1 by A1, A6, FINSEQ_2:49 ;
len z = n by A1, NUMBER13:def 1;
then k + 1 in dom z by A5, FINSEQ_3:25;
then z /. (k + 1) = z . (k + 1) by PARTFUN1:def 6
.= primenumber k by A1, A2, NUMBER13:def 1 ;
hence eval ((LagPoly (i,z)),(In ((k + 1),F_Rat))) = primenumber k by A7, A6, A3, Th59; :: thesis: verum