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 that
A1: m >= 1 and
A2: k >= 2 ; :: thesis: (SDDec (M0 r)) + (SDDec (DecSD (0,(m + 2),k))) = (SDDec (Mmin r)) + (SDDec (SDMax ((m + 2),m,k)))
A3: m + 2 > 1 by A1, Lm1;
(SDDec (M0 r)) + (SDDec (SDMin ((m + 2),m,k))) = (SDDec (Mmin r)) + (SDDec (DecSD (0,(m + 2),k))) by A2, Th11
.= (SDDec (Mmin r)) + 0 by A3, 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 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