for k being Nat st k >= 2 holds
SD_Add_Carry (Radix k) = 1