:: deftheorem Def3 defines Card_Intersection CARD_FIN:def 4 :
for k being Nat
for F being finite-yielding Function st dom F is finite holds
for b₃ being Element of NAT holds
( b₃ = Card_Intersection (F,k) iff for x, y being object
for X being finite set
for P being Function of (card (Choose (X,k,x,y))),(Choose (X,k,x,y)) st dom F = X & P is one-to-one & x <> y holds
ex 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 (F,f,x)) ) & b₃ = Sum XFS ) );