theorem :: RLVECT_3:28

for M being non empty set
for CF being Choice_Function of M st not {} in M holds
dom CF = M by Lm7;