let k be Nat; :: thesis: for x being Integer holds (SD_Add_Data (x,k)) + ((SD_Add_Carry x) * (Radix k)) = x
let x be Integer; :: thesis: (SD_Add_Data (x,k)) + ((SD_Add_Carry x) * (Radix k)) = x
(SD_Add_Data (x,k)) + ((SD_Add_Carry x) * (Radix k)) = (x - ((SD_Add_Carry x) * (Radix k))) + ((SD_Add_Carry x) * (Radix k)) by RADIX_1:def 11;
hence (SD_Add_Data (x,k)) + ((SD_Add_Carry x) * (Radix k)) = x ; :: thesis: verum