let x be object ; :: thesis: apply ({},x) = <*x*>
( len (apply ({},x)) = 0 + 1 & (apply ({},x)) . 1 = x ) by Def4, CARD_1:27;
hence apply ({},x) = <*x*> by FINSEQ_1:40; :: thesis: verum