theorem Th7: :: AOFA_I00:7

for X being set
for f being Function holds
( f is Denumeration of X iff ( dom f = card X & rng f = X & f is one-to-one ) )