theorem Th12: :: RADIX_6:12

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