for P being non empty mutually-disjoint with_non-empty_elements set
for f being Choice_Function of P holds f is one-to-one