for n being Nat st n >= 1 holds
for k, x, y being Nat st k >= 2 & x is_represented_by n,k & y is_represented_by n,k holds
x + y = (SDDec ((DecSD (x,n,k)) '+' (DecSD (y,n,k)))) + (((Radix k) |^ n) * (SD_Add_Carry ((DigA ((DecSD (x,n,k)),n)) + (DigA ((DecSD (y,n,k)),n)))))