theorem Th9: :: RADIX_1:10

for k being Nat holds k -SD c= (k + 1) -SD