theorem Th1: :: RADIX_6:1

for n being Nat st n >= 1 holds
for m, k being Nat st m >= 1 & k >= 2 holds
SDDec (Fmin ((m + n),m,k)) = SDDec (Fmin (m,m,k))