theorem Th56: :: CARD_FIN:57

for Fy being finite-yielding Function
for X being finite set
for n, k being Nat st dom Fy = X & ex x, y being set st
( x <> y & ( for f being Function st f in Choose (X,k,x,y) holds
card (Intersection (Fy,f,x)) = n ) ) holds
Card_Intersection (Fy,k) = n * ((card X) choose k)