let m, k be Nat; :: thesis: for r being Tuple of (m + 2),(k -SD ) st m >= 1 & k >= 2 holds
(SDDec (M0 r)) + (SDDec (DecSD 0 ,(m + 2),k)) = (SDDec (Mmin r)) + (SDDec (SDMax (m + 2),m,k))
let r be Tuple of (m + 2),(k -SD ); :: thesis: ( m >= 1 & k >= 2 implies (SDDec (M0 r)) + (SDDec (DecSD 0 ,(m + 2),k)) = (SDDec (Mmin r)) + (SDDec (SDMax (m + 2),m,k)) )
assume A1: ( m >= 1 & k >= 2 ) ; :: thesis: (SDDec (M0 r)) + (SDDec (DecSD 0 ,(m + 2),k)) = (SDDec (Mmin r)) + (SDDec (SDMax (m + 2),m,k))
then A2: m + 2 > 1 by Lm1;
A3: m in Seg (m + 2) by A1, FINSEQ_3:10;
(SDDec (M0 r)) + (SDDec (SDMin (m + 2),m,k)) = (SDDec (Mmin r)) + (SDDec (DecSD 0 ,(m + 2),k)) by A1, Th11
.= (SDDec (Mmin r)) + 0 by A2, RADIX_5:6 ;
then (SDDec (Mmin r)) + (SDDec (SDMax (m + 2),m,k)) = (SDDec (M0 r)) + ((SDDec (SDMax (m + 2),m,k)) + (SDDec (SDMin (m + 2),m,k)))
.= (SDDec (M0 r)) + (SDDec (DecSD 0 ,(m + 2),k)) by A1, A2, A3, RADIX_5:17 ;
hence (SDDec (M0 r)) + (SDDec (DecSD 0 ,(m + 2),k)) = (SDDec (Mmin r)) + (SDDec (SDMax (m + 2),m,k)) ; :: thesis: verum