theorem Th63: :: NUMBER19:63

for n, k being Nat st 1 <= k & k <= n holds
for z being FinSequence of INT.Ring st z = idseq n holds
( eval ((LagIPoly (z,k)),(In (k,INT.Ring))) = (((- 1) |^ (n -' k)) * ((n -' k) !)) * ((k -' 1) !) & ( for i being Nat st 1 <= i & i <= n & i <> k holds
In (i,INT.Ring) is_a_root_of LagIPoly (z,k) ) )