let E be Enumeration of X; :: thesis: ( E is card X -element & E is X -valued )
A1: rng E = X by RLAFFIN3:def 1;
Seg (len E) = dom E by FINSEQ_1:def 3;
then len E = card (dom E) ;
hence ( E is card X -element & E is X -valued ) by A1, RELAT_1:def 19, CARD_1:70, CARD_1:def 7; :: thesis: verum