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

( 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