:: deftheorem Def1 defines Choose CARD_FIN:def 1 :
for X being finite set
for k being Nat
for x1, x2 being object
for b₅ being Subset of (Funcs (X,{x1,x2})) holds
( b₅ = Choose (X,k,x1,x2) iff for x being set holds
( x in b₅ iff ex f being Function of X,{x1,x2} st
( f = x & card (f " {x1}) = k ) ) );