let A be included_in_Seg set ; :: thesis: dom (Sgm A) = Seg (card A)
len (Sgm A) = card A by Th37;
hence dom (Sgm A) = Seg (card A) by FINSEQ_1:def 3; :: thesis: verum