let m, k be Nat; :: thesis: ( m >= 1 & k >= 2 implies for r being Tuple of m + 2,k -SD holds SDDec (M0 r) < (SDDec (Mmin r)) + (SDDec (Fmin (m + 2),m,k)) )
assume that
A1: m >= 1 and
A2: k >= 2 ; :: thesis: for r being Tuple of m + 2,k -SD holds SDDec (M0 r) < (SDDec (Mmin r)) + (SDDec (Fmin (m + 2),m,k))
let r be Tuple of m + 2,k -SD ; :: thesis: SDDec (M0 r) < (SDDec (Mmin r)) + (SDDec (Fmin (m + 2),m,k))
A3: m + 2 > 1 by A1, Lm1;
A4: (SDDec (Mmin r)) + (SDDec (SDMax (m + 2),m,k)) = (SDDec (M0 r)) + (SDDec (DecSD 0 ,(m + 2),k)) by A1, A2, Th12
.= (SDDec (M0 r)) + 0 by A3, RADIX_5:6 ;
A5: (SDDec (M0 r)) + 1 > (SDDec (M0 r)) + 0 by XREAL_1:10;
m in Seg (m + 2) by A1, FINSEQ_3:10;
then SDDec (Fmin (m + 2),m,k) = (SDDec (SDMax (m + 2),m,k)) + (SDDec (DecSD 1,(m + 2),k)) by A2, A3, RADIX_5:18
.= (SDDec (SDMax (m + 2),m,k)) + 1 by A2, A3, RADIX_5:9 ;
hence SDDec (M0 r) < (SDDec (Mmin r)) + (SDDec (Fmin (m + 2),m,k)) by A4, A5; :: thesis: verum