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) )
assume A1: x1 <> x2 ; :: thesis: 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

let x be set ; :: 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 set 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 set st x = [y,z]
then consider y being Function of E,{x1,x2}, z being Subset of E such that
A2: ( x = [y,z] & card (y " {x1}) = k & y " {x1} = z ) ;
reconsider y = y, z = z as set ;
take y = y; :: thesis: ex z being set st x = [y,z]
take z = z; :: thesis: x = [y,z]
thus x = [y,z] by A2; :: 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

let x, y1, y2 be set ; :: 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
A3: ( [x,y1] = [fX1,X1] & card (fX1 " {x1}) = k & fX1 " {x1} = X1 ) ;
assume [x,y2] in f ; :: thesis: y1 = y2
then consider fX2 being Function of E,{x1,x2}, X2 being Subset of E such that
A4: ( [x,y2] = [fX2,X2] & card (fX2 " {x1}) = k & fX2 " {x1} = X2 ) ;
A5: ( x = fX1 & y1 = X1 ) by A3, ZFMISC_1:33;
( x = fX2 & y2 = X2 ) by A4, ZFMISC_1:33;
hence y1 = y2 by A3, A4, A5; :: thesis: verum

end;

then reconsider f = f as Function by FUNCT_1:def 1;

now

let y1, y2 be set ; :: thesis: ( y1 in dom f & y2 in dom f & f . y1 = f . y2 implies y1 = y2 )
assume A6: ( y1 in dom f & y2 in dom f ) ; :: thesis: ( f . y1 = f . y2 implies y1 = y2 )
assume A7: f . y1 = f . y2 ; :: thesis: y1 = y2
[y1,(f . y1)] in f by A6, FUNCT_1:8;
then consider fX1 being Function of E,{x1,x2}, X1 being Subset of E such that
A8: ( [y1,(f . y1)] = [fX1,X1] & card (fX1 " {x1}) = k & fX1 " {x1} = X1 ) ;
[y2,(f . y2)] in f by A6, FUNCT_1:8;
then consider fX2 being Function of E,{x1,x2}, X2 being Subset of E such that
A9: ( [y2,(f . y2)] = [fX2,X2] & card (fX2 " {x1}) = k & fX2 " {x1} = X2 ) ;
A10: ( y1 = fX1 & f . y1 = X1 ) by A8, ZFMISC_1:33;
A11: ( y2 = fX2 & f . y2 = X2 ) by A9, ZFMISC_1:33;
A12: fX1 " {x1} = fX2 " {x1} by A7, A8, A9, A10, ZFMISC_1:33;
dom fX1 = E by FUNCT_2:def 1;
then A13: dom fX1 = dom fX2 by FUNCT_2:def 1;
for z being set st z in dom fX1 holds
fX1 . z = fX2 . z

proof

assume ex z being set st
( z in dom fX1 & fX1 . z <> fX2 . z ) ; :: thesis: contradiction
then consider z being set such that
A14: ( z in dom fX1 & fX1 . z <> fX2 . z ) ;
A15: fX1 . z in {x1,x2} by A14, FUNCT_2:7;
fX2 . z in {x1,x2} by A14, FUNCT_2:7;
then A16: ( 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 A14, A15, A16, TARSKI:def 2;

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

A18: [z,(fX1 . z)] in fX1 by A14, FUNCT_1:8;
fX1 . z in {x1} by A17, TARSKI:def 1;
then z in fX2 " {x1} by A12, A18, RELAT_1:def 14;
then consider z' being set such that
A19: ( [z,z'] in fX2 & z' in {x1} ) by RELAT_1:def 14;
z' = fX2 . z by A19, FUNCT_1:8;
hence contradiction by A1, A17, A19, TARSKI:def 1; :: thesis: verum

end;

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

A21: [z,(fX2 . z)] in fX2 by A13, A14, FUNCT_1:8;
fX2 . z in {x1} by A20, TARSKI:def 1;
then z in fX1 " {x1} by A12, A21, RELAT_1:def 14;
then consider z' being set such that
A22: ( [z,z'] in fX1 & z' in {x1} ) by RELAT_1:def 14;
z' = fX1 . z by A22, FUNCT_1:8;
hence contradiction by A1, A20, A22, TARSKI:def 1; :: thesis: verum

end;

end;

end;

hence y1 = y2 by A10, A11, A13, FUNCT_1:9; :: thesis: verum

end;

then A23: f is one-to-one by FUNCT_1:def 8;
for x being set holds
( x in Choose E,k,x1,x2 iff ex y being set st [x,y] in f )

proof

let x be set ; :: thesis: ( x in Choose E,k,x1,x2 iff ex y being set st [x,y] in f )
thus ( x in Choose E,k,x1,x2 implies ex y being set st [x,y] in f ) :: thesis: ( ex y being set 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 set st [x,y] in f
then consider fX being Function of E,{x1,x2} such that
A24: ( 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 A24; :: thesis: verum

end;

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

proof

given y being set such that A25: [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
A26: ( [x,y] = [fX,X] & card (fX " {x1}) = k & fX " {x1} = X ) by A25;
x = fX by A26, ZFMISC_1:33;
hence x in Choose E,k,x1,x2 by A26, CARD_FIN:def 1; :: thesis: verum

end;

end;

then A27: dom f = Choose E,k,x1,x2 by RELAT_1:def 4;
for y being set holds
( y in the_subsets_of_card k,E iff ex x being set st [x,y] in f )

proof

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

hereby :: thesis: ( ex x being set 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 set st [x,y] in f
then consider X being Subset of E such that
A28: ( y = X & card X = k ) ;
defpred S₁[ set , set ] means ( ( $1 in X & $2 = x1 ) or ( not $1 in X & $2 = x2 ) );
A29: 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 A30: 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 A30; :: thesis: verum

end;

suppose A31: 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 A31; :: 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(A29);
then consider f' being Function of E,{x1,x2} such that
A32: for z being Element of E holds S₁[z,f' . z] ;
reconsider x = f' as set ;
take x = x; :: thesis: [x,y] in f

now

let z be set ; :: thesis: ( ( z in X implies z in f' " {x1} ) & ( z in f' " {x1} implies z in X ) )

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

assume A33: z in X ; :: thesis: z in f' " {x1}
then z in E ;
then z in dom f' by FUNCT_2:def 1;
then A34: [z,(f' . z)] in f' by FUNCT_1:8;
reconsider z' = z as Element of E by A33;
A35: f' . z' = x1 by A32, A33;
set z'' = f' . z';
f' . z' in {x1} by A35, TARSKI:def 1;
hence z in f' " {x1} by A34, RELAT_1:def 14; :: thesis: verum

end;

assume z in f' " {x1} ; :: thesis: z in X
then consider z' being set such that
A36: ( [z,z'] in f' & z' in {x1} ) by RELAT_1:def 14;
A37: z' = x1 by A36, TARSKI:def 1;
z in dom f' by A36, RELAT_1:def 4;
then reconsider z'' = z as Element of E ;
f' . z'' = x1 by A36, A37, FUNCT_1:8;
hence z in X by A1, A32; :: thesis: verum

end;

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

end;

given x being set such that A38: [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
A39: ( [x,y] = [fX,X] & card (fX " {x1}) = k & fX " {x1} = X ) by A38;
( card X = k & y = X ) by A39, ZFMISC_1:33;
hence y in the_subsets_of_card k,E ; :: thesis: verum

end;

then rng f = the_subsets_of_card k,E by RELAT_1:def 5;
then Choose E,k,x1,x2, the_subsets_of_card k,E are_equipotent by A23, A27, WELLORD2:def 4;
hence card (Choose E,k,x1,x2) = card (the_subsets_of_card k,E) by CARD_1:21; :: thesis: verum