let X be set ; :: thesis: ( X is countable iff ex f being Function st
( dom f = omega & X c= rng f ) )
thus ( X is countable implies ex f being Function st
( dom f = omega & X c= rng f ) ) :: thesis: ( ex f being Function st
( dom f = omega & X c= rng f ) implies X is countable )

proof

assume card X c= omega ; :: according to CARD_3:def 14 :: thesis: ex f being Function st
( dom f = omega & X c= rng f )
hence ex f being Function st
( dom f = omega & X c= rng f ) by CARD_1:12, CARD_1:47; :: thesis: verum

end;

assume ex f being Function st
( dom f = omega & X c= rng f ) ; :: thesis: X is countable
hence card X c= omega by CARD_1:12, CARD_1:47; :: according to CARD_3:def 14 :: thesis: verum