let x1, x2 be set ; :: thesis: for X being finite set holds card (Choose (X,(card X),x1,x2)) = 1
let X be finite set ; :: thesis: card (Choose (X,(card X),x1,x2)) = 1

per cases ( X is empty or not X is empty ) ;

suppose A1: X is empty ; :: thesis: card (Choose (X,(card X),x1,x2)) = 1

A2: rng {} = {} ;
dom {} = X by A1;
then reconsider Empty = {} as Function of X,{x1,x2} by A2, FUNCT_2:2, XBOOLE_1:2;
A3: Choose (X,(card X),x1,x2) c= {Empty}

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in Choose (X,(card X),x1,x2) or z in {Empty} )
assume z in Choose (X,(card X),x1,x2) ; :: thesis: z in {Empty}
then consider f being Function of X,{x1,x2} such that
A4: z = f and
card (f " {x1}) = card X by Def1;
dom f = X by FUNCT_2:def 1;
then f = Empty ;
hence z in {Empty} by A4, TARSKI:def 1; :: thesis: verum

end;

Empty " {x1} = {} by FUNCT_1:72, RELAT_1:38;
then Empty in Choose (X,(card X),x1,x2) by A1, Def1;
then Choose (X,(card X),x1,x2) = {Empty} by A3, ZFMISC_1:33;
hence card (Choose (X,(card X),x1,x2)) = 1 by CARD_1:30; :: thesis: verum

end;

suppose A5: not X is empty ; :: thesis: card (Choose (X,(card X),x1,x2)) = 1

then consider f being Function such that
A6: dom f = X and
A7: rng f = {x1} by FUNCT_1:5;
rng f c= {x1,x2} by A7, ZFMISC_1:36;
then A8: f is Function of X,{x1,x2} by A6, FUNCT_2:2;
A9: Choose (X,(card X),x1,x2) c= {f}

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in Choose (X,(card X),x1,x2) or z in {f} )
assume z in Choose (X,(card X),x1,x2) ; :: thesis: z in {f}
then consider g being Function of X,{x1,x2} such that
A10: z = g and
A11: card (g " {x1}) = card X by Def1;

A12: now

per cases ( x1 = x2 or x1 <> x2 ) ;

suppose x1 = x2 ; :: thesis: rng g = {x1}

then {x1,x2} = {x1} by ENUMSET1:29;
hence rng g = {x1} by A5, ZFMISC_1:33; :: thesis: verum

end;

suppose A13: x1 <> x2 ; :: thesis: rng g = {x1}

g " {x2} = {}

proof

assume g " {x2} <> {} ; :: thesis: contradiction
then consider z being set such that
A14: z in g " {x2} by XBOOLE_0:def 1;
g . z in {x2} by A14, FUNCT_1:def 7;
then A15: g . z = x2 by TARSKI:def 1;
g " {x1} = X by A11, Th1;
then g . z in {x1} by A14, FUNCT_1:def 7;
hence contradiction by A13, A15, TARSKI:def 1; :: thesis: verum

end;

then not x2 in rng g by FUNCT_1:72;
then ( not rng g = {x2} & not rng g = {x1,x2} ) by TARSKI:def 1, TARSKI:def 2;
hence rng g = {x1} by A5, ZFMISC_1:36; :: thesis: verum

end;

end;

end;

dom g = X by FUNCT_2:def 1;
then g = f by A6, A7, A12, FUNCT_1:7;
hence z in {f} by A10, TARSKI:def 1; :: thesis: verum

end;

card (f " {x1}) = card X by A6, A7, RELAT_1:134;
then f in Choose (X,(card X),x1,x2) by A8, Def1;
then Choose (X,(card X),x1,x2) = {f} by A9, ZFMISC_1:33;
hence card (Choose (X,(card X),x1,x2)) = 1 by CARD_1:30; :: thesis: verum

end;

end;