theorem Th22: :: AFINSQ_2:22

for n being Nat holds (Sgm0 {n}) . 0 = n