let X be finite set ; :: thesis: for x1, x2 being object holds card (Choose (X,(card X),x1,x2)) = 1
let x1, x2 be object ; :: 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

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

proof

let z be object ; :: 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
A3: 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 A3, TARSKI:def 1; :: thesis: verum

end;

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

end;

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

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

proof

let z be object ; :: 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
A9: z = g and
A10: card (g " {x1}) = card X by Def1;

A11: now :: thesis: rng g = {x1}

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 A4, ZFMISC_1:33; :: thesis: verum

end;

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

g " {x2} = {}

proof

assume g " {x2} <> {} ; :: thesis: contradiction
then consider z being object such that
A13: z in g " {x2} by XBOOLE_0:def 1;
g . z in {x2} by A13, FUNCT_1:def 7;
then A14: g . z = x2 by TARSKI:def 1;
g " {x1} = X by A10, CARD_2:102;
then g . z in {x1} by A13, FUNCT_1:def 7;
hence contradiction by A12, A14, 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 A4, ZFMISC_1:36; :: thesis: verum

end;

end;

end;

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

end;

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

end;

end;