for n, k being Nat
for X being set
for F being Function of (the_subsets_of_card (n,X)),k st k <> 0 & X is infinite holds
ex H being Subset of X st
( H is infinite & F | (the_subsets_of_card (n,H)) is constant )