let k be natural number ; :: thesis: for A being finite set st A c= Seg k holds
dom (Sgm A) = Seg (card A)
let A be finite set ; :: thesis: ( A c= Seg k implies dom (Sgm A) = Seg (card A) )
assume A c= Seg k ; :: thesis: dom (Sgm A) = Seg (card A)
then ( len (Sgm A) = card A & dom (Sgm A) = Seg (len (Sgm A)) ) by Th44, FINSEQ_1:def 3;
hence dom (Sgm A) = Seg (card A) ; :: thesis: verum