theorem Th8: :: RADIX_2:8

for k being Nat
for x being Integer holds (SD_Add_Data (x,k)) + ((SD_Add_Carry x) * (Radix k)) = x