theorem Th12: :: CARD_FIN:13

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