let x1 be set ; :: thesis: for X being finite set
for k being Element of NAT st card X <> k holds
Choose X,k,x1,x1 is empty
let X be finite set ; :: thesis: for k being Element of NAT st card X <> k holds
Choose X,k,x1,x1 is empty
let k be Element of 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 set such that
A2: y in Choose X,k,x1,x1 by XBOOLE_0:def 1;
consider f being Function of X,{x1,x1} such that
A3: ( f = y & card (f " {x1}) = k ) by A2, Def1;

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

suppose rng f is empty ; :: thesis: contradiction

then ( card (f " {x1}) = 0 & dom f = {} & dom f = X ) by CARD_1:47, FUNCT_1:142, FUNCT_2:def 1, RELAT_1:65;
hence contradiction by A1, A3; :: thesis: verum

end;

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

( rng f c= {x1,x1} & {x1,x1} = {x1} ) by ENUMSET1:69;
then rng f = {x1} by A4, ZFMISC_1:39;
then ( f " {x1} = dom f & dom f = X ) by FUNCT_2:def 1, RELAT_1:169;
hence contradiction by A1, A3; :: thesis: verum

end;

end;