theorem Th15: :: RADIX_3:15

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