theorem :: AOFA_I00:10

for X being non empty set
for f being Denumeration of X holds f . 0 in X by FUNCT_2:5, ORDINAL3:8;