theorem Th2: :: RADIX_3:2

for k being Nat holds k -SD_Sub_S c= k -SD_Sub