theorem :: RADIX_5:19

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