theorem :: RADIX_5:18

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