let m, k be Nat; :: thesis: ( m >= 1 & k >= 2 implies for r being Tuple of (m + 2),(k -SD ) holds (SDDec (Mmax r)) + (SDDec (DecSD 0 ,(m + 2),k)) = (SDDec (M0 r)) + (SDDec (SDMax (m + 2),m,k)) )
assume A1: ( m >= 1 & k >= 2 ) ; :: thesis: for r being Tuple of (m + 2),(k -SD ) holds (SDDec (Mmax r)) + (SDDec (DecSD 0 ,(m + 2),k)) = (SDDec (M0 r)) + (SDDec (SDMax (m + 2),m,k))
A2: m + 2 >= 1 by NAT_1:12;
let r be Tuple of (m + 2),(k -SD ); :: thesis: (SDDec (Mmax r)) + (SDDec (DecSD 0 ,(m + 2),k)) = (SDDec (M0 r)) + (SDDec (SDMax (m + 2),m,k))
for i being Nat holds
( not i in Seg (m + 2) or ( DigA (M0 r),i = DigA (Mmax r),i & DigA (SDMax (m + 2),m,k),i = 0 ) or ( DigA (SDMax (m + 2),m,k),i = DigA (Mmax r),i & DigA (M0 r),i = 0 ) )

proof

let i be Nat; :: thesis: ( not i in Seg (m + 2) or ( DigA (M0 r),i = DigA (Mmax r),i & DigA (SDMax (m + 2),m,k),i = 0 ) or ( DigA (SDMax (m + 2),m,k),i = DigA (Mmax r),i & DigA (M0 r),i = 0 ) )
assume A3: i in Seg (m + 2) ; :: thesis: ( ( DigA (M0 r),i = DigA (Mmax r),i & DigA (SDMax (m + 2),m,k),i = 0 ) or ( DigA (SDMax (m + 2),m,k),i = DigA (Mmax r),i & DigA (M0 r),i = 0 ) )
then A4: ( i >= 1 & i <= m + 2 ) by FINSEQ_1:3;
A5: DigA (Mmax r),i = MmaxDigit r,i by A3, Def4;

now

per cases ( i < m or i >= m ) ;

suppose A6: i < m ; :: thesis: ( ( DigA (M0 r),i = DigA (Mmax r),i & DigA (SDMax (m + 2),m,k),i = 0 ) or ( DigA (SDMax (m + 2),m,k),i = DigA (Mmax r),i & DigA (M0 r),i = 0 ) )

then A7: DigA (Mmax r),i = (Radix k) - 1 by A1, A3, A5, Def3
.= SDMaxDigit m,k,i by A1, A4, A6, RADIX_5:def 3
.= DigA (SDMax (m + 2),m,k),i by A3, RADIX_5:def 4 ;
DigA (M0 r),i = M0Digit r,i by A3, Def2
.= 0 by A3, A6, Def1 ;
hence ( ( DigA (M0 r),i = DigA (Mmax r),i & DigA (SDMax (m + 2),m,k),i = 0 ) or ( DigA (SDMax (m + 2),m,k),i = DigA (Mmax r),i & DigA (M0 r),i = 0 ) ) by A7; :: thesis: verum

end;

suppose A8: i >= m ; :: thesis: ( ( DigA (M0 r),i = DigA (Mmax r),i & DigA (SDMax (m + 2),m,k),i = 0 ) or ( DigA (SDMax (m + 2),m,k),i = DigA (Mmax r),i & DigA (M0 r),i = 0 ) )

then A9: DigA (Mmax r),i = r . i by A1, A3, A5, Def3
.= M0Digit r,i by A3, A8, Def1
.= DigA (M0 r),i by A3, Def2 ;
DigA (SDMax (m + 2),m,k),i = SDMaxDigit m,k,i by A3, RADIX_5:def 4
.= 0 by A1, A8, RADIX_5:def 3 ;
hence ( ( DigA (M0 r),i = DigA (Mmax r),i & DigA (SDMax (m + 2),m,k),i = 0 ) or ( DigA (SDMax (m + 2),m,k),i = DigA (Mmax r),i & DigA (M0 r),i = 0 ) ) by A9; :: thesis: verum

end;

end;

end;

hence ( ( DigA (M0 r),i = DigA (Mmax r),i & DigA (SDMax (m + 2),m,k),i = 0 ) or ( DigA (SDMax (m + 2),m,k),i = DigA (Mmax r),i & DigA (M0 r),i = 0 ) ) ; :: thesis: verum

end;

hence (SDDec (Mmax r)) + (SDDec (DecSD 0 ,(m + 2),k)) = (SDDec (M0 r)) + (SDDec (SDMax (m + 2),m,k)) by A1, A2, RADIX_5:15; :: thesis: verum