let x1, x2 be set ; :: thesis: for X being finite set st x1 <> x2 holds
card (Choose X,0 ,x1,x2) = 1
let X be finite set ; :: thesis: ( x1 <> x2 implies card (Choose X,0 ,x1,x2) = 1 )
assume A1: x1 <> x2 ; :: thesis: card (Choose X,0 ,x1,x2) = 1

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

suppose X is empty ; :: thesis: card (Choose X,0 ,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 A3: Empty in Choose X,0 ,x1,x2 by Def1;
Choose X,0 ,x1,x2 c= {Empty}

proof

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

end;

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

end;

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

then consider f being Function such that
A7: ( dom f = X & rng f = {x2} ) by FUNCT_1:15;
( not x1 in rng f & rng f c= {x1,x2} ) by A1, A7, TARSKI:def 1, ZFMISC_1:42;
then ( f " {x1} = {} & f is Function of X,{x1,x2} & card {} = 0 ) by A7, FUNCT_1:142, FUNCT_2:4;
then A8: f in Choose X,0 ,x1,x2 by Def1;
Choose X,0 ,x1,x2 c= {f}

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in Choose X,0 ,x1,x2 or z in {f} )
assume A9: z in Choose X,0 ,x1,x2 ; :: thesis: z in {f}
consider g being Function of X,{x1,x2} such that
A10: ( z = g & card (g " {x1}) = 0 ) by A9, Def1;
g " {x1} = {} by A10;
then ( not x1 in rng g & dom g = X ) by FUNCT_1:142, FUNCT_2:def 1;
then ( rng g <> {} & not rng g = {x1} & not rng g = {x1,x2} ) by A6, TARSKI:def 1, TARSKI:def 2;
then ( dom g = X & rng g = {x2} ) by FUNCT_2:def 1, ZFMISC_1:42;
then g = f by A7, FUNCT_1:17;
hence z in {f} by A10, TARSKI:def 1; :: thesis: verum

end;

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

end;

end;