theorem Th37: :: FINSEQ_3:39

for k being Nat
for A being finite set st A c= Seg k holds
len (Sgm A) = card A