theorem Th17: :: RADIX_1:18

SD_Add_Carry 0 = 0 by Def10;