for M being set st ( for X being set st X in M holds
X <> {} ) holds
ex f being Function st
( dom f = M & ( for X being set st X in M holds
f . X in X ) )