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 by Th44;
hence dom (Sgm A) = Seg (card A) by FINSEQ_1:def 3; :: thesis: verum