theorem Th61: :: CARD_FIN:62

for X being finite set
for F being Function st dom F = X & F is one-to-one holds
ex XF being XFinSequence of INT st
( Sum XF = card { h where h is Function of X,(rng F) : ( h is one-to-one & ( for x being set st x in X holds
h . x <> F . x ) ) } & dom XF = (card X) + 1 & ( for n being Nat st n in dom XF holds
XF . n = (((- 1) |^ n) * ((card X) !)) / (n !) ) )