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

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

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in Choose (X,0,x1,x2) or z in {Empty} )
assume z in Choose (X,0,x1,x2) ; :: thesis: z in {Empty}
then consider f being Function of X,{x1,x2} such that
A4: z = f and
card (f " {x1}) = 0 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} = {} & card {} = 0 ) ;
then Empty in Choose (X,0,x1,x2) by Def1;
then Choose (X,0,x1,x2) = {Empty} by A3, ZFMISC_1:33;
hence card (Choose (X,0,x1,x2)) = 1 by CARD_1:30; :: thesis: verum

end;

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

then consider f being Function such that
A6: dom f = X and
A7: rng f = {x2} 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,0,x1,x2) c= {f}

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in Choose (X,0,x1,x2) or z in {f} )
assume z in Choose (X,0,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}) = 0 by Def1;
g " {x1} = {} by A11;
then not x1 in rng g by FUNCT_1:72;
then ( not rng g = {x1} & not rng g = {x1,x2} ) by TARSKI:def 1, TARSKI:def 2;
then ( dom g = X & rng g = {x2} ) by A5, FUNCT_2:def 1, ZFMISC_1:36;
then g = f by A6, A7, FUNCT_1:7;
hence z in {f} by A10, TARSKI:def 1; :: thesis: verum

end;

not x1 in rng f by A1, A7, TARSKI:def 1;
then A12: f " {x1} = {} by FUNCT_1:72;
card {} = 0 ;
then f in Choose (X,0,x1,x2) by A12, A8, Def1;
then Choose (X,0,x1,x2) = {f} by A9, ZFMISC_1:33;
hence card (Choose (X,0,x1,x2)) = 1 by CARD_1:30; :: thesis: verum

end;

end;