theorem Th13: :: CARD_FIN:14

for X being finite set
for k being Nat
for z, x, y being object st not z in X & x <> y holds
card (Choose (X,k,x,y)) = card { f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k & f . z = y ) }