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