let x1 be set ; :: thesis: for X being finite set
for k being Nat st card X <> k holds
Choose (X,k,x1,x1) is empty
let X be finite set ; :: thesis: for k being Nat st card X <> k holds
Choose (X,k,x1,x1) is empty
let k be Nat; :: thesis: ( card X <> k implies Choose (X,k,x1,x1) is empty )
assume A1: card X <> k ; :: thesis: Choose (X,k,x1,x1) is empty
assume not Choose (X,k,x1,x1) is empty ; :: thesis: contradiction
then consider y being object such that
A2: y in Choose (X,k,x1,x1) ;
consider f being Function of X,{x1,x1} such that
f = y and
A3: card (f " {x1}) = k by A2, Def1;

per cases ( rng f is empty or not rng f is empty ) ;

suppose A4: rng f is empty ; :: thesis: contradiction

A5: dom f = X by FUNCT_2:def 1;
dom f = {} by A4, RELAT_1:42;
hence contradiction by A1, A3, A5; :: thesis: verum

end;

suppose A6: not rng f is empty ; :: thesis: contradiction

{x1,x1} = {x1} by ENUMSET1:29;
then rng f = {x1} by A6, ZFMISC_1:33;
then f " {x1} = dom f by RELAT_1:134;
hence contradiction by A1, A3, FUNCT_2:def 1; :: thesis: verum

end;

end;