theorem Th13: :: RADIX_6:13

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