theorem :: RADIX_5:17

for n being Nat st n >= 1 holds
for m, k being Nat st k >= 2 holds
(SDDec (SDMax (n,m,k))) + (SDDec (SDMin (n,m,k))) = SDDec (DecSD (0,n,k))