for k, m, n being Nat st m is_represented_by 1,k & n is_represented_by 1,k holds
SD_Add_Carry ((DigA ((DecSD (m,1,k)),1)) + (DigA ((DecSD (n,1,k)),1))) = SD_Add_Carry (m + n)