let x be object ; :: thesis: for E being Enumeration of {x} holds E = <*x*>
let E be Enumeration of {x}; :: thesis: E = <*x*>
A1: ( len E = card {x} & card {x} = 1 ) by CARD_1:def 7;
then 1 in dom E by FINSEQ_3:25;
then E . 1 in rng E by FUNCT_1:def 3;
then E . 1 = x by TARSKI:def 1;
hence E = <*x*> by A1, FINSEQ_1:40; :: thesis: verum