theorem Th11: :: RADIX_6:11

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