let A be finite natural-membered set ; :: thesis: len (Sgm0 A) = card A
rng (Sgm0 A) = A by Def4;
then len (Sgm0 A),A are_equipotent by WELLORD2:def 4;
then card A = card (len (Sgm0 A)) by CARD_1:5;
hence len (Sgm0 A) = card A ; :: thesis: verum