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 {n} c= Seg n by ZFMISC_1:37;
then ( rng (Sgm {n}) = {n} & len (Sgm {n}) = card {n} ) by Th44, FINSEQ_1:def 13;
then ( rng (Sgm {n}) = {n} & len (Sgm {n}) = 1 ) by CARD_1:50;
hence Sgm {n} = <*n*> by FINSEQ_1:56; :: thesis: verum