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