theorem Th3: :: RADIX_3:3

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