theorem :: AOFA_I00:9

for X being non empty set
for x being Element of X ex f being Enumeration of X st f . x = 0