theorem Th7: :: RADIX_4:7

for k, x, n being Nat st k >= 2 holds
((Radix k) |^ n) * (DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1))) = ((((Radix k) |^ n) * (DigA ((DecSD (x,(n + 1),k)),(n + 1)))) - (((Radix k) |^ (n + 1)) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),(n + 1))),k)))) + (((Radix k) |^ n) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),n)),k)))