let X be finite set ; :: thesis: canFS X is Enumeration of X
rng (canFS X) = X by FUNCT_2:def 3;
hence canFS X is Enumeration of X by RLAFFIN3:def 1; :: thesis: verum