theorem Th16: :: RADIX_3:16

for k being Nat holds SDSub_Add_Carry (0,k) = 0