let X be finite set ; :: thesis: for n being Nat holds card { Y where Y is Subset of X : card Y = n } = (card X) choose n
let n be Nat; :: thesis: card { Y where Y is Subset of X : card Y = n } = (card X) choose n
reconsider N = n as Element of NAT by ORDINAL1:def 13;
set YY = { Y where Y is Subset of X : card Y = n } ;
set CH = Choose X,N,1,0 ;
deffunc H₁( set ) -> set = (X --> 0 ) +* ($1 --> 1);
consider f being Function such that
A1: ( dom f = { Y where Y is Subset of X : card Y = n } & ( for x being set st x in { Y where Y is Subset of X : card Y = n } holds
f . x = H₁(x) ) ) from FUNCT_1:sch 3();
A2: rng f c= Choose X,N,1,0

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in Choose X,N,1,0 )
assume y in rng f ; :: thesis: y in Choose X,N,1,0
then consider x being set such that
A3: ( x in dom f & f . x = y ) by FUNCT_1:def 5;
consider Y being Subset of X such that
A4: ( x = Y & card Y = n ) by A1, A3;
Y \/ X = X by XBOOLE_1:12;
then H₁(Y) in Choose X,N,1,0 by A4, CARD_FIN:19;
hence y in Choose X,N,1,0 by A1, A3, A4; :: thesis: verum

end;

A5: Choose X,N,1,0 c= rng f

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in Choose X,N,1,0 or y in rng f )
assume y in Choose X,N,1,0 ; :: thesis: y in rng f
then consider g being Function of X,{0 ,1} such that
A6: ( g = y & card (g " {1}) = n ) by CARD_FIN:def 1;
X = dom g by FUNCT_2:def 1;
then reconsider Y = g " {1} as Subset of X by RELAT_1:167;
( dom (Y --> 1) = Y & dom (X --> 0 ) = X ) by FUNCOP_1:19;
then A7: dom H₁(Y) = X \/ Y by FUNCT_4:def 1
.= X by XBOOLE_1:12 ;
A8: dom g = X by FUNCT_2:def 1;

now

let x be set ; :: thesis: ( x in dom g implies g . x = H₁(Y) . x )
assume A9: x in dom g ; :: thesis: g . x = H₁(Y) . x

now

per cases ( x in Y or not x in Y ) ;

suppose x in Y ; :: thesis: g . x = H₁(Y) . x

then ( g . x in {1} & x in dom (Y --> 1) & (Y --> 1) . x = 1 ) by FUNCOP_1:13, FUNCOP_1:19, FUNCT_1:def 13;
then ( g . x = 1 & H₁(Y) . x = 1 ) by FUNCT_4:14, TARSKI:def 1;
hence g . x = H₁(Y) . x ; :: thesis: verum

end;

suppose A10: not x in Y ; :: thesis: g . x = H₁(Y) . x

then ( not g . x in {1} & g . x in rng g & rng g c= {0 ,1} ) by A9, FUNCT_1:def 5, FUNCT_1:def 13, RELAT_1:def 19;
then ( (X --> 0 ) . x = 0 & dom (Y --> 1) = Y & g . x <> 1 & g . x in {0 ,1} ) by A9, FUNCOP_1:13, FUNCOP_1:19, TARSKI:def 1;
then ( H₁(Y) . x = 0 & g . x = 0 ) by A10, FUNCT_4:12, TARSKI:def 2;
hence g . x = H₁(Y) . x ; :: thesis: verum

end;

end;

end;

hence g . x = H₁(Y) . x ; :: thesis: verum

end;

then ( H₁(Y) = g & Y in { Y where Y is Subset of X : card Y = n } ) by A6, A7, A8, FUNCT_1:9;
then ( f . Y = g & f . Y in rng f ) by A1, FUNCT_1:def 5;
hence y in rng f by A6; :: thesis: verum

end;

for x1, x2 being set st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2

proof

let x1, x2 be set ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume A11: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 ) ; :: thesis: x1 = x2
consider Y1 being Subset of X such that
A12: ( x1 = Y1 & card Y1 = n ) by A1, A11;
consider Y2 being Subset of X such that
A13: ( x2 = Y2 & card Y2 = n ) by A1, A11;
Y1 c= Y2

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in Y1 or y in Y2 )
assume A14: y in Y1 ; :: thesis: y in Y2
assume A15: not y in Y2 ; :: thesis: contradiction
( dom (Y1 --> 1) = Y1 & (Y1 --> 1) . y = 1 & dom (Y2 --> 1) = Y2 & (X --> 0 ) . y = 0 ) by A14, FUNCOP_1:13, FUNCOP_1:19;
then ( H₁(Y1) . y = 1 & H₁(Y2) . y = 0 & H₁(Y1) = f . x1 & H₁(Y2) = f . x2 ) by A1, A11, A12, A13, A14, A15, FUNCT_4:12, FUNCT_4:14;
hence contradiction by A11; :: thesis: verum

end;

hence x1 = x2 by A12, A13, CARD_FIN:1; :: thesis: verum

end;

then ( f is without_repeated_line & rng f = Choose X,N,1,0 ) by A2, A5, FUNCT_1:def 8, XBOOLE_0:def 10;
then { Y where Y is Subset of X : card Y = n } , Choose X,N,1,0 are_equipotent by A1, WELLORD2:def 4;
then card { Y where Y is Subset of X : card Y = n } = card (Choose X,N,1,0 ) by CARD_1:21;
hence card { Y where Y is Subset of X : card Y = n } = (card X) choose n by CARD_FIN:18; :: thesis: verum