theorem Th17: :: RADIX_6:17

for m, k being Nat
for r being Tuple of m + 2,k -SD st k >= 2 holds
(SDDec (M0 r)) + (SDDec (Mmask r)) = (SDDec r) + (SDDec (DecSD (0,(m + 2),k)))