theorem Th38: :: FINSEQ_3:40

for A being included_in_Seg set holds dom (Sgm A) = Seg (card A)