let A be non empty set ; :: thesis: ( A is countable implies ex f being Function st
( dom f = NAT & A = rng f ) )
assume A1: A is countable ; :: thesis: ex f being Function st
( dom f = NAT & A = rng f )
A c= A ;
then consider F being sequence of A such that
A2: A = rng F by A1, SUPINF_2:def 8;
dom F = NAT by FUNCT_2:def 1;
hence ex f being Function st
( dom f = NAT & A = rng f ) by A2; :: thesis: verum