for k, n being Nat st n >= 1 holds
for m being Nat st m is_represented_by n,k holds
m = SDDec (DecSD (m,n,k))