theorem Th58: :: CARD_FIN:59

for X, Y being finite set st not X is empty & not Y is empty holds
ex F being XFinSequence of INT st
( dom F = (card Y) + 1 & Sum F = card { f where f is Function of X,Y : f is onto } & ( for n being Nat st n in dom F holds
F . n = (((- 1) |^ n) * ((card Y) choose n)) * (((card Y) - n) |^ (card X)) ) )