let X be countable set ; :: thesis: for f being Enumeration of X holds rng f c= NAT
let f be Enumeration of X; :: thesis: rng f c= NAT
card X c= NAT by CARD_3:def 15;
hence rng f c= NAT by ThNum1; :: thesis: verum