for k being Nat
for Fy being finite-yielding Function
for x, y being set
for X being finite set
for P being Function of (card (Choose (X,k,x,y))),(Choose (X,k,x,y)) st dom Fy = X & P is one-to-one & x <> y holds
for XFS being XFinSequence of NAT st dom XFS = dom P & ( for z being set
for f being Function st z in dom XFS & f = P . z holds
XFS . z = card (Intersection (Fy,f,x)) ) holds
Card_Intersection (Fy,k) = Sum XFS