let x, y be set ; :: thesis: for X being finite set
for k being Nat st x <> y holds
card (Choose (X,k,x,y)) = (card X) choose k
let X be finite set ; :: thesis: for k being Nat st x <> y holds
card (Choose (X,k,x,y)) = (card X) choose k
let k be Nat; :: thesis: ( x <> y implies card (Choose (X,k,x,y)) = (card X) choose k )
defpred S₁[ Nat] means for k being Nat
for X being finite set st k + (card X) <= $1 holds
card (Choose (X,k,x,y)) = (card X) choose k;
assume A1: x <> y ; :: thesis: card (Choose (X,k,x,y)) = (card X) choose k
A2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
let k be Nat; :: thesis: for X being finite set st k + (card X) <= n + 1 holds
card (Choose (X,k,x,y)) = (card X) choose k
let X be finite set ; :: thesis: ( k + (card X) <= n + 1 implies card (Choose (X,k,x,y)) = (card X) choose k )
assume A4: k + (card X) <= n + 1 ; :: thesis: card (Choose (X,k,x,y)) = (card X) choose k

per cases ( k + (card X) < n + 1 or k + (card X) = n + 1 ) by A4, XXREAL_0:1;

suppose k + (card X) < n + 1 ; :: thesis: card (Choose (X,k,x,y)) = (card X) choose k

then k + (card X) <= n by NAT_1:13;
hence card (Choose (X,k,x,y)) = (card X) choose k by A3; :: thesis: verum

end;

suppose A5: k + (card X) = n + 1 ; :: thesis: card (Choose (X,k,x,y)) = (card X) choose k

per cases ( ( k = 0 & card X >= 0 ) or ( k > 0 & card X = 0 ) or ( k > 0 & card X > 0 ) ) ;

suppose A6: ( k = 0 & card X >= 0 ) ; :: thesis: card (Choose (X,k,x,y)) = (card X) choose k

then card (Choose (X,k,x,y)) = 1 by A1, Th11;
hence card (Choose (X,k,x,y)) = (card X) choose k by A6, NEWTON:29; :: thesis: verum

end;

suppose A7: ( k > 0 & card X = 0 ) ; :: thesis: card (Choose (X,k,x,y)) = (card X) choose k

then Choose (X,k,x,y) is empty by Th10;
hence card (Choose (X,k,x,y)) = (card X) choose k by A7, NEWTON:def 3; :: thesis: verum

end;

suppose A8: ( k > 0 & card X > 0 ) ; :: thesis: card (Choose (X,k,x,y)) = (card X) choose k

then reconsider cXz = (card X) - 1 as Element of NAT by NAT_1:20;
reconsider k1 = k - 1 as Element of NAT by A8, NAT_1:20;
consider z being set such that
A9: z in X by A8, CARD_1:47, XBOOLE_0:def 1;
set Xz = X \ {z};
z in {z} by TARSKI:def 1;
then A10: not z in X \ {z} by XBOOLE_0:def 5;
(X \ {z}) \/ {z} = X by A9, ZFMISC_1:140;
then A11: card (Choose (X,(k1 + 1),x,y)) = (card (Choose ((X \ {z}),(k1 + 1),x,y))) + (card (Choose ((X \ {z}),k1,x,y))) by A1, A10, Th17;
card X = cXz + 1 ;
then A12: card (X \ {z}) = cXz by A9, STIRL2_1:65;
cXz < cXz + 1 by NAT_1:13;
then A13: card (X \ {z}) < card X by A9, STIRL2_1:65;
then k + (card (X \ {z})) < n + 1 by A5, XREAL_1:10;
then k + (card (X \ {z})) <= n by NAT_1:13;
then A14: card (Choose ((X \ {z}),(k1 + 1),x,y)) = (card (X \ {z})) choose (k1 + 1) by A3;
k1 < k1 + 1 by NAT_1:13;
then k1 + (card (X \ {z})) < n + 1 by A5, A13, XREAL_1:10;
then k1 + (card (X \ {z})) <= n by NAT_1:13;
then A15: card (Choose ((X \ {z}),k1,x,y)) = (card (X \ {z})) choose k1 by A3;
card X = cXz + 1 ;
hence card (Choose (X,k,x,y)) = (card X) choose k by A14, A15, A11, A12, NEWTON:32; :: thesis: verum

end;

end;

end;

end;

end;

A16: S₁[ 0 ]

proof

let k be Nat; :: thesis: for X being finite set st k + (card X) <= 0 holds
card (Choose (X,k,x,y)) = (card X) choose k
let X be finite set ; :: thesis: ( k + (card X) <= 0 implies card (Choose (X,k,x,y)) = (card X) choose k )
X: 0 choose 0 = 1 by NEWTON:29;
assume k + (card X) <= 0 ; :: thesis: card (Choose (X,k,x,y)) = (card X) choose k
then ( k + (card X) = 0 & card X = 0 ) ;
hence card (Choose (X,k,x,y)) = (card X) choose k by A1, Th11, X; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A16, A2);
then S₁[k + (card X)] ;
hence card (Choose (X,k,x,y)) = (card X) choose k ; :: thesis: verum