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