theorem Th42: :: FINSEQ_3:44

for n being Nat st 0 <> n holds
Sgm {n} = <*n*>