theorem :: RADIX_3:19

for k being Nat
for i1, i2 being Integer st 2 <= k & i1 in k -SD & i2 in k -SD_Sub holds
SDSub_Add_Data ((i1 + i2),k) in k -SD_Sub_S