let x, y be set ; :: thesis: for X being finite set
for k being Element of NAT st x <> y holds
card (Choose X,k,x,y) = (card X) choose k
let X be finite set ; :: thesis: for k being Element of NAT st x <> y holds
card (Choose X,k,x,y) = (card X) choose k
let k be Element of NAT ; :: thesis: ( x <> y implies 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
defpred S₁[ Element of NAT ] means for k being Element of NAT
for X being finite set st k + (card X) <= $1 holds
card (Choose X,k,x,y) = (card X) choose k;
A2: S₁[ 0 ]

proof

let k be Element of 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 )
assume A3: k + (card X) <= 0 ; :: thesis: card (Choose X,k,x,y) = (card X) choose k
k + (card X) = 0 by A3;
then ( card X = 0 & k = 0 ) ;
hence card (Choose X,k,x,y) = (card X) choose k by A1, Th11, NEWTON:27; :: thesis: verum

end;

A4: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A5: S₁[n] ; :: thesis: S₁[n + 1]
let k be Element of 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 A6: 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 A6, 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 A5; :: thesis: verum

end;

suppose A7: 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 ( k = 0 & card X >= 0 ) ; :: thesis: card (Choose X,k,x,y) = (card X) choose k

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

end;

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

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

end;

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

then reconsider k1 = k - 1 as Element of NAT by NAT_1:20;
reconsider cXz = (card X) - 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};
( card X = cXz + 1 & cXz < cXz + 1 ) by NAT_1:13;
then ( card (X \ {z}) < card X & k1 < k1 + 1 ) by A9, NAT_1:13, STIRL2_1:65;
then ( k + (card (X \ {z})) < n + 1 & k1 + (card (X \ {z})) < n + 1 & z in {z} ) by A7, TARSKI:def 1, XREAL_1:10;
then ( k + (card (X \ {z})) <= n & k1 + (card (X \ {z})) <= n & (X \ {z}) \/ {z} = X & not z in X \ {z} & card X = cXz + 1 ) by A9, NAT_1:13, XBOOLE_0:def 5, ZFMISC_1:140;
then ( card (Choose (X \ {z}),(k1 + 1),x,y) = (card (X \ {z})) choose (k1 + 1) & card (Choose (X \ {z}),k1,x,y) = (card (X \ {z})) choose k1 & card (Choose X,(k1 + 1),x,y) = (card (Choose (X \ {z}),(k1 + 1),x,y)) + (card (Choose (X \ {z}),k1,x,y)) & card (X \ {z}) = cXz & card X = cXz + 1 ) by A1, A5, A9, Th17, STIRL2_1:65;
hence card (Choose X,k,x,y) = (card X) choose k by NEWTON:32; :: thesis: verum

end;

end;

end;

end;

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A2, A4);
then S₁[k + (card X)] ;
hence card (Choose X,k,x,y) = (card X) choose k ; :: thesis: verum