let n be natural number ; :: thesis: ( 0 <> n implies Sgm {n} = <*n*> )
assume 0 <> n ; :: thesis: Sgm {n} = <*n*>
then n in Seg n by FINSEQ_1:5;
then A1: {n} c= Seg n by ZFMISC_1:37;
then len (Sgm {n}) = card {n} by Th44;
then A2: len (Sgm {n}) = 1 by CARD_1:50;
rng (Sgm {n}) = {n} by A1, FINSEQ_1:def 13;
hence Sgm {n} = <*n*> by A2, FINSEQ_1:56; :: thesis: verum