theorem :: RADIX_4:9

for n being Nat st n >= 1 holds
for k, x, y being Nat st k >= 3 & x is_represented_by n,k & y is_represented_by n,k holds
x + y = SDSub2IntOut ((SD2SDSub (DecSD (x,n,k))) '+' (SD2SDSub (DecSD (y,n,k))))