theorem Th57: :: CARD_FIN:58

for Fy being finite-yielding Function
for X being finite set st dom Fy = X holds
for XF being XFinSequence of NAT st dom XF = card X & ( for n being Nat st n in dom XF holds
ex x, y being set st
( x <> y & ( for f being Function st f in Choose (X,(n + 1),x,y) holds
card (Intersection (Fy,f,x)) = XF . n ) ) ) holds
ex F being XFinSequence of INT st
( dom F = card X & card (union (rng Fy)) = Sum F & ( for n being Nat st n in dom F holds
F . n = (((- 1) |^ n) * (XF . n)) * ((card X) choose (n + 1)) ) )