let n be Nat; :: thesis: ( 0 <> n implies Sgm {n} = <*n*> )
assume 0 <> n ; :: thesis: Sgm {n} = <*n*>
then n in Seg n by FINSEQ_1:3;
then A1: {n} c= Seg n by ZFMISC_1:31;
then len (Sgm {n}) = card {n} by Th37;
then A2: len (Sgm {n}) = 1 by CARD_1:30;
rng (Sgm {n}) = {n} by A1, FINSEQ_1:def 13;
hence Sgm {n} = <*n*> by A2, FINSEQ_1:39; :: thesis: verum