let k be natural number ; :: thesis: for A being finite set st A c= Seg k holds
len (Sgm A) = card A
let A be finite set ; :: thesis: ( A c= Seg k implies len (Sgm A) = card A )
assume A c= Seg k ; :: thesis: len (Sgm A) = card A
then ( dom (Sgm A) = Seg (len (Sgm A)) & rng (Sgm A) = A & Sgm A is one-to-one ) by Lm1, FINSEQ_1:def 3, FINSEQ_1:def 13;
then ( Seg (len (Sgm A)),A are_equipotent & Seg (len (Sgm A)) is finite ) by WELLORD2:def 4;
then ( card (Seg (len (Sgm A))) = len (Sgm A) & card A = card (Seg (len (Sgm A))) ) by CARD_1:21, FINSEQ_1:78;
hence len (Sgm A) = card A ; :: thesis: verum