let E be non empty finite set ; :: thesis: for k being Element of NAT
for x1, x2 being set st x1 <> x2 holds
card (Choose (E,k,x1,x2)) = card (the_subsets_of_card (k,E))
let k be Element of NAT ; :: thesis: for x1, x2 being set st x1 <> x2 holds
card (Choose (E,k,x1,x2)) = card (the_subsets_of_card (k,E))
let x1, x2 be set ; :: thesis: ( x1 <> x2 implies card (Choose (E,k,x1,x2)) = card (the_subsets_of_card (k,E)) )
set f = { [fX,X] where fX is Function of E,{x1,x2}, X is Subset of E : ( card (fX " {x1}) = k & fX " {x1} = X ) } ;

now :: thesis: for x being object st x in { [fX,X] where fX is Function of E,{x1,x2}, X is Subset of E : ( card (fX " {x1}) = k & fX " {x1} = X ) } holds
ex y, z being object st x = [y,z]

let x be object ; :: thesis: ( x in { [fX,X] where fX is Function of E,{x1,x2}, X is Subset of E : ( card (fX " {x1}) = k & fX " {x1} = X ) } implies ex y, z being object st x = [y,z] )
assume x in { [fX,X] where fX is Function of E,{x1,x2}, X is Subset of E : ( card (fX " {x1}) = k & fX " {x1} = X ) } ; :: thesis: ex y, z being object st x = [y,z]
then consider y being Function of E,{x1,x2}, z being Subset of E such that
A1: x = [y,z] and
card (y " {x1}) = k and
y " {x1} = z ;
reconsider y = y, z = z as object ;
take y = y; :: thesis: ex z being object st x = [y,z]
take z = z; :: thesis: x = [y,z]
thus x = [y,z] by A1; :: thesis: verum

end;

then reconsider f = { [fX,X] where fX is Function of E,{x1,x2}, X is Subset of E : ( card (fX " {x1}) = k & fX " {x1} = X ) } as Relation-like set by RELAT_1:def 1;

now :: thesis: for x, y1, y2 being object st [x,y1] in f & [x,y2] in f holds
y1 = y2

let x, y1, y2 be object ; :: thesis: ( [x,y1] in f & [x,y2] in f implies y1 = y2 )
assume [x,y1] in f ; :: thesis: ( [x,y2] in f implies y1 = y2 )
then consider fX1 being Function of E,{x1,x2}, X1 being Subset of E such that
A2: [x,y1] = [fX1,X1] and
card (fX1 " {x1}) = k and
A3: fX1 " {x1} = X1 ;
A4: x = fX1 by A2, XTUPLE_0:1;
assume [x,y2] in f ; :: thesis: y1 = y2
then consider fX2 being Function of E,{x1,x2}, X2 being Subset of E such that
A5: [x,y2] = [fX2,X2] and
card (fX2 " {x1}) = k and
A6: fX2 " {x1} = X2 ;
x = fX2 by A5, XTUPLE_0:1;
hence y1 = y2 by A2, A3, A5, A6, A4, XTUPLE_0:1; :: thesis: verum

end;

then reconsider f = f as Function by FUNCT_1:def 1;
assume A7: x1 <> x2 ; :: thesis: card (Choose (E,k,x1,x2)) = card (the_subsets_of_card (k,E))

now :: thesis: for y1, y2 being object st y1 in dom f & y2 in dom f & f . y1 = f . y2 holds
y1 = y2

let y1, y2 be object ; :: thesis: ( y1 in dom f & y2 in dom f & f . y1 = f . y2 implies y1 = y2 )
assume that
A8: y1 in dom f and
A9: y2 in dom f ; :: thesis: ( f . y1 = f . y2 implies y1 = y2 )
assume A10: f . y1 = f . y2 ; :: thesis: y1 = y2
[y2,(f . y2)] in f by A9, FUNCT_1:1;
then consider fX2 being Function of E,{x1,x2}, X2 being Subset of E such that
A11: [y2,(f . y2)] = [fX2,X2] and
card (fX2 " {x1}) = k and
A12: fX2 " {x1} = X2 ;
A13: y2 = fX2 by A11, XTUPLE_0:1;
[y1,(f . y1)] in f by A8, FUNCT_1:1;
then consider fX1 being Function of E,{x1,x2}, X1 being Subset of E such that
A14: [y1,(f . y1)] = [fX1,X1] and
card (fX1 " {x1}) = k and
A15: fX1 " {x1} = X1 ;
dom fX1 = E by FUNCT_2:def 1;
then A16: dom fX1 = dom fX2 by FUNCT_2:def 1;
f . y1 = X1 by A14, XTUPLE_0:1;
then A17: fX1 " {x1} = fX2 " {x1} by A10, A15, A11, A12, XTUPLE_0:1;
A18: for z being object st z in dom fX1 holds
fX1 . z = fX2 . z

proof

given z being object such that A19: z in dom fX1 and
A20: fX1 . z <> fX2 . z ; :: thesis: contradiction
A21: fX1 . z in {x1,x2} by A19, FUNCT_2:5;
fX2 . z in {x1,x2} by A19, FUNCT_2:5;
then A22: ( fX2 . z = x1 or fX2 . z = x2 ) by TARSKI:def 2;

per cases ( ( fX1 . z = x1 & fX2 . z = x2 ) or ( fX1 . z = x2 & fX2 . z = x1 ) ) by A20, A21, A22, TARSKI:def 2;

suppose A23: ( fX1 . z = x1 & fX2 . z = x2 ) ; :: thesis: contradiction

then A24: fX1 . z in {x1} by TARSKI:def 1;
[z,(fX1 . z)] in fX1 by A19, FUNCT_1:1;
then z in fX2 " {x1} by A17, A24, RELAT_1:def 14;
then consider z9 being object such that
A25: [z,z9] in fX2 and
A26: z9 in {x1} by RELAT_1:def 14;
z9 = fX2 . z by A25, FUNCT_1:1;
hence contradiction by A7, A23, A26, TARSKI:def 1; :: thesis: verum

end;

suppose A27: ( fX1 . z = x2 & fX2 . z = x1 ) ; :: thesis: contradiction

then A28: fX2 . z in {x1} by TARSKI:def 1;
[z,(fX2 . z)] in fX2 by A16, A19, FUNCT_1:1;
then z in fX1 " {x1} by A17, A28, RELAT_1:def 14;
then consider z9 being object such that
A29: [z,z9] in fX1 and
A30: z9 in {x1} by RELAT_1:def 14;
z9 = fX1 . z by A29, FUNCT_1:1;
hence contradiction by A7, A27, A30, TARSKI:def 1; :: thesis: verum

end;

end;

end;

y1 = fX1 by A14, XTUPLE_0:1;
hence y1 = y2 by A13, A16, A18, FUNCT_1:2; :: thesis: verum

end;

then A31: f is one-to-one by FUNCT_1:def 4;
for y being object holds
( y in the_subsets_of_card (k,E) iff ex x being object st [x,y] in f )

proof

let y be object ; :: thesis: ( y in the_subsets_of_card (k,E) iff ex x being object st [x,y] in f )

hereby :: thesis: ( ex x being object st [x,y] in f implies y in the_subsets_of_card (k,E) )

assume y in the_subsets_of_card (k,E) ; :: thesis: ex x being object st [x,y] in f
then consider X being Subset of E such that
A32: ( y = X & card X = k ) ;
defpred S₁[ set , set ] means ( ( $1 in X & $2 = x1 ) or ( not $1 in X & $2 = x2 ) );
A33: for z1 being Element of E ex z2 being Element of {x1,x2} st S₁[z1,z2]

proof

let z1 be Element of E; :: thesis: ex z2 being Element of {x1,x2} st S₁[z1,z2]

per cases ( z1 in X or not z1 in X ) ;

suppose A34: z1 in X ; :: thesis: ex z2 being Element of {x1,x2} st S₁[z1,z2]

reconsider z2 = x1 as Element of {x1,x2} by TARSKI:def 2;
take z2 ; :: thesis: S₁[z1,z2]
thus S₁[z1,z2] by A34; :: thesis: verum

end;

suppose A35: not z1 in X ; :: thesis: ex z2 being Element of {x1,x2} st S₁[z1,z2]

reconsider z2 = x2 as Element of {x1,x2} by TARSKI:def 2;
take z2 ; :: thesis: S₁[z1,z2]
thus S₁[z1,z2] by A35; :: thesis: verum

end;

end;

end;

ex f being Function of E,{x1,x2} st
for z being Element of E holds S₁[z,f . z] from FUNCT_2:sch 3(A33);
then consider f9 being Function of E,{x1,x2} such that
A36: for z being Element of E holds S₁[z,f9 . z] ;
reconsider x = f9 as object ;
take x = x; :: thesis: [x,y] in f

now :: thesis: for z being object holds
( ( z in X implies z in f9 " {x1} ) & ( z in f9 " {x1} implies z in X ) )

let z be object ; :: thesis: ( ( z in X implies z in f9 " {x1} ) & ( z in f9 " {x1} implies z in X ) )

hereby :: thesis: ( z in f9 " {x1} implies z in X )

assume A37: z in X ; :: thesis: z in f9 " {x1}
then reconsider z9 = z as Element of E ;
set z99 = f9 . z9;
z in E by A37;
then z in dom f9 by FUNCT_2:def 1;
then A38: [z,(f9 . z)] in f9 by FUNCT_1:1;
f9 . z9 = x1 by A36, A37;
then f9 . z9 in {x1} by TARSKI:def 1;
hence z in f9 " {x1} by A38, RELAT_1:def 14; :: thesis: verum

end;

assume z in f9 " {x1} ; :: thesis: z in X
then consider z9 being object such that
A39: [z,z9] in f9 and
A40: z9 in {x1} by RELAT_1:def 14;
z in dom f9 by A39, XTUPLE_0:def 12;
then reconsider z99 = z as Element of E ;
z9 = x1 by A40, TARSKI:def 1;
then f9 . z99 = x1 by A39, FUNCT_1:1;
hence z in X by A7, A36; :: thesis: verum

end;

then X = f9 " {x1} by TARSKI:2;
hence [x,y] in f by A32; :: thesis: verum

end;

given x being object such that A41: [x,y] in f ; :: thesis: y in the_subsets_of_card (k,E)
consider fX being Function of E,{x1,x2}, X being Subset of E such that
A42: [x,y] = [fX,X] and
A43: ( card (fX " {x1}) = k & fX " {x1} = X ) by A41;
y = X by A42, XTUPLE_0:1;
hence y in the_subsets_of_card (k,E) by A43; :: thesis: verum

end;

then A44: rng f = the_subsets_of_card (k,E) by XTUPLE_0:def 13;
for x being object holds
( x in Choose (E,k,x1,x2) iff ex y being object st [x,y] in f )

proof

let x be object ; :: thesis: ( x in Choose (E,k,x1,x2) iff ex y being object st [x,y] in f )
thus ( x in Choose (E,k,x1,x2) implies ex y being object st [x,y] in f ) :: thesis: ( ex y being object st [x,y] in f implies x in Choose (E,k,x1,x2) )

proof

assume x in Choose (E,k,x1,x2) ; :: thesis: ex y being object st [x,y] in f
then consider fX being Function of E,{x1,x2} such that
A45: ( fX = x & card (fX " {x1}) = k ) by CARD_FIN:def 1;
set y = fX " {x1};
take fX " {x1} ; :: thesis: [x,(fX " {x1})] in f
thus [x,(fX " {x1})] in f by A45; :: thesis: verum

end;

thus ( ex y being object st [x,y] in f implies x in Choose (E,k,x1,x2) ) :: thesis: verum

proof

given y being object such that A46: [x,y] in f ; :: thesis: x in Choose (E,k,x1,x2)
consider fX being Function of E,{x1,x2}, X being Subset of E such that
A47: [x,y] = [fX,X] and
A48: card (fX " {x1}) = k and
fX " {x1} = X by A46;
x = fX by A47, XTUPLE_0:1;
hence x in Choose (E,k,x1,x2) by A48, CARD_FIN:def 1; :: thesis: verum

end;

end;

then dom f = Choose (E,k,x1,x2) by XTUPLE_0:def 12;
then Choose (E,k,x1,x2), the_subsets_of_card (k,E) are_equipotent by A31, A44;
hence card (Choose (E,k,x1,x2)) = card (the_subsets_of_card (k,E)) by CARD_1:5; :: thesis: verum