let m, k be Nat; :: thesis: for r being Tuple of (m + 2),(k -SD ) st m >= 1 & k >= 2 & SDDec (Mmask r) > 0 holds
SDDec r > SDDec (M0 r)
let r be Tuple of (m + 2),(k -SD ); :: thesis: ( m >= 1 & k >= 2 & SDDec (Mmask r) > 0 implies SDDec r > SDDec (M0 r) )
assume A1: ( m >= 1 & k >= 2 ) ; :: thesis: ( not SDDec (Mmask r) > 0 or SDDec r > SDDec (M0 r) )
then A2: m + 2 > 1 by Lm1;
assume A3: SDDec (Mmask r) > 0 ; :: thesis: SDDec r > SDDec (M0 r)
(SDDec (M0 r)) + (SDDec (Mmask r)) = (SDDec r) + (SDDec (DecSD 0 ,(m + 2),k)) by A1, Th17
.= (SDDec r) + 0 by A2, RADIX_5:6 ;
then (SDDec r) - (SDDec (M0 r)) = (SDDec (Mmask r)) - 0 ;
hence SDDec r > SDDec (M0 r) by A3, XREAL_1:49; :: thesis: verum