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

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