let k be Nat; :: 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 )
A1: dom (Sgm A) = Seg (len (Sgm A)) by FINSEQ_1:def 3;
A2: card (Seg (len (Sgm A))) = len (Sgm A) by FINSEQ_1:57;
assume A3: A c= Seg k ; :: thesis: len (Sgm A) = card A
then A4: rng (Sgm A) = A by FINSEQ_1:def 13;
Sgm A is one-to-one by A3, Lm1;
then Seg (len (Sgm A)),A are_equipotent by A1, A4;
hence len (Sgm A) = card A by A2, CARD_1:5; :: thesis: verum