for k, x, n being Nat st n >= 1 & k >= 3 & x is_represented_by n + 1,k holds
DigA_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1)) = SDSub_Add_Carry ((DigA ((DecSD (x,n,k)),n)),k)