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

then ( dom {} = X & rng {} = {} & {} c= {x1,x2} ) by XBOOLE_1:2;
then reconsider Empty = {} as Function of X,{x1,x2} by FUNCT_2:4;
( Empty " {x1} = {} & card {} = 0 ) by FUNCT_1:142, RELAT_1:60;
then A2: Empty in Choose X,(card X),x1,x2 by A1, Def1;
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 A3: z in Choose X,(card X),x1,x2 ; :: thesis: z in {Empty}
consider f being Function of X,{x1,x2} such that
A4: ( z = f & card (f " {x1}) = card X ) by A3, Def1;
dom f = X by FUNCT_2:def 1;
then f = Empty ;
hence z in {Empty} by A4, TARSKI:def 1; :: thesis: verum

end;

then Choose X,(card X),x1,x2 = {Empty} by A2, ZFMISC_1:39;
hence card (Choose X,(card X),x1,x2) = 1 by CARD_1:50; :: 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 & rng f = {x1} ) by FUNCT_1:15;
( rng f c= {x1,x2} & f " {x1} = X ) by A6, RELAT_1:169, ZFMISC_1:42;
then ( f is Function of X,{x1,x2} & card (f " {x1}) = card X ) by A6, FUNCT_2:4;
then A7: f in Choose X,(card X),x1,x2 by Def1;
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 A8: z in Choose X,(card X),x1,x2 ; :: thesis: z in {f}
consider g being Function of X,{x1,x2} such that
A9: ( z = g & card (g " {x1}) = card X ) by A8, Def1;

now

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

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

( rng g <> {} & rng g c= {x1,x2} & {x1,x2} = {x1} ) by A5, A10, ENUMSET1:69;
hence rng g = {x1} by ZFMISC_1:39; :: thesis: verum

end;

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

g " {x2} = {}

proof

assume g " {x2} <> {} ; :: thesis: contradiction
then consider z being set such that
A12: z in g " {x2} by XBOOLE_0:def 1;
( z in dom g & g . z in {x2} & g " {x1} = X ) by A9, A12, Th1, FUNCT_1:def 13;
then ( g . z in {x1} & g . z = x2 ) by FUNCT_1:def 13, TARSKI:def 1;
hence contradiction by A11, TARSKI:def 1; :: thesis: verum

end;

then ( not x2 in rng g & dom g = X ) by FUNCT_1:142, FUNCT_2:def 1;
then ( rng g <> {} & not rng g = {x2} & not rng g = {x1,x2} ) by A5, TARSKI:def 1, TARSKI:def 2;
hence rng g = {x1} by ZFMISC_1:42; :: thesis: verum

end;

end;

end;

then ( dom g = X & rng g = {x1} ) by FUNCT_2:def 1;
then g = f by A6, FUNCT_1:17;
hence z in {f} by A9, TARSKI:def 1; :: thesis: verum

end;

then Choose X,(card X),x1,x2 = {f} by A7, ZFMISC_1:39;
hence card (Choose X,(card X),x1,x2) = 1 by CARD_1:50; :: thesis: verum

end;

end;