theorem Th2: :: RADIX_4:2

for x, y being Integer
for k being Nat st 3 <= k holds
SDSub_Add_Carry (((SDSub_Add_Carry (x,k)) + (SDSub_Add_Carry (y,k))),k) = 0