theorem Th20: :: AFINSQ_2:20

for A being finite natural-membered set holds len (Sgm0 A) = card A