theorem Th4: :: RADIX_4:4

for m, k being Nat st 2 <= k & m is_represented_by 1,k holds
DigA_SDSub ((SD2SDSub (DecSD (m,1,k))),(1 + 1)) = SDSub_Add_Carry (m,k)