let A be finite natural-membered set ; :: thesis: len (Sgm0 A) = card A
( dom (Sgm0 A) = len (Sgm0 A) & rng (Sgm0 A) = A & Sgm0 A is one-to-one ) by AC113;
then ( len (Sgm0 A),A are_equipotent & len (Sgm0 A) is finite ) by WELLORD2:def 4;
then ( card (len (Sgm0 A)) = len (Sgm0 A) & card A = card (len (Sgm0 A)) ) by CARD_1:21;
hence len (Sgm0 A) = card A ; :: thesis: verum