theorem Th54: :: CARD_FIN:55

for Fy being finite-yielding Function
for X being finite set ex XFS being XFinSequence of INT st
( dom XFS = card X & ( for n being Nat st n in dom XFS holds
XFS . n = ((- 1) |^ n) * (Card_Intersection (Fy,(n + 1))) ) )