let x be set ; :: thesis: apply {} ,x = <*x*>
( len (apply {} ,x) = 0 + 1 & (apply {} ,x) . 1 = x ) by Def5, CARD_1:47;
hence apply {} ,x = <*x*> by FINSEQ_1:57; :: thesis: verum