theorem Th3: :: RADIX_4:3

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