theorem Th38: :: FINSEQ_3:40

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