let m, k be Nat; 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 ; ( 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
; (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)))
; verum