let X be set ; :: thesis: for f being Function holds
( f is Enumeration of X iff ( dom f = X & rng f = card X & f is one-to-one ) )
let f be Function; :: thesis: ( f is Enumeration of X iff ( dom f = X & rng f = card X & f is one-to-one ) )
( card X = {} implies X = {} ) ;
hence ( f is Enumeration of X iff ( dom f = X & rng f = card X & f is one-to-one ) ) by FUNCT_2:2, FUNCT_2:def 1, FUNCT_2:def 3; :: thesis: verum