theorem :: CARD_FIN:60

for n, k being Nat st k <= n holds
ex F being XFinSequence of INT st
( n block k = (1 / (k !)) * (Sum F) & dom F = k + 1 & ( for m being Nat st m in dom F holds
F . m = (((- 1) |^ m) * (k choose m)) * ((k - m) |^ n) ) )