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 14;
hence rng f c= NAT ; :: thesis: verum