theorem Th14: :: CARD_FIN:15

for X being finite set
for k being Nat
for z, x, y being object st x <> y & not z in X holds
card (Choose ((X \/ {z}),(k + 1),x,y)) = (card (Choose (X,(k + 1),x,y))) + (card (Choose (X,k,x,y)))