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