theorem Th9: :: RADIX_6:9

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