for i1, i2 being Integer
for k being Nat st k >= 2 & i1 in k -SD & i2 in k -SD holds
( (- (Radix k)) + 2 <= SD_Add_Data ((i1 + i2),k) & SD_Add_Data ((i1 + i2),k) <= (Radix k) - 2 )