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

( 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