theorem :: NUMBER19:64

for n being Nat
for y being b₁ -element FinSequence of INT ex p being Polynomial of INT.Ring st
for k being Nat st 1 <= k & k <= n holds
eval (p,(In (k,INT.Ring))) = 1 + ((((k -' 1) !) * ((n -' k) !)) * (y . k))