let m, k be Nat; :: thesis: ( k >= 2 implies for r being Tuple of m + 2,k -SD holds (SDDec (Mmin r)) + (SDDec (DecSD (0,(m + 2),k))) = (SDDec (M0 r)) + (SDDec (SDMin ((m + 2),m,k))) )
assume A1: k >= 2 ; :: thesis: for r being Tuple of m + 2,k -SD holds (SDDec (Mmin r)) + (SDDec (DecSD (0,(m + 2),k))) = (SDDec (M0 r)) + (SDDec (SDMin ((m + 2),m,k)))
let r be Tuple of m + 2,k -SD ; :: thesis: (SDDec (Mmin r)) + (SDDec (DecSD (0,(m + 2),k))) = (SDDec (M0 r)) + (SDDec (SDMin ((m + 2),m,k)))
A2: for i being Nat holds
( not i in Seg (m + 2) or ( DigA ((M0 r),i) = DigA ((Mmin r),i) & DigA ((SDMin ((m + 2),m,k)),i) = 0 ) or ( DigA ((SDMin ((m + 2),m,k)),i) = DigA ((Mmin 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 ((Mmin r),i) & DigA ((SDMin ((m + 2),m,k)),i) = 0 ) or ( DigA ((SDMin ((m + 2),m,k)),i) = DigA ((Mmin r),i) & DigA ((M0 r),i) = 0 ) )
assume A3: i in Seg (m + 2) ; :: thesis: ( ( DigA ((M0 r),i) = DigA ((Mmin r),i) & DigA ((SDMin ((m + 2),m,k)),i) = 0 ) or ( DigA ((SDMin ((m + 2),m,k)),i) = DigA ((Mmin r),i) & DigA ((M0 r),i) = 0 ) )
then A4: DigA ((Mmin r),i) = MminDigit (r,i) by Def6;
A5: i >= 1 by A3, FINSEQ_1:1;

now :: thesis: ( ( DigA ((M0 r),i) = DigA ((Mmin r),i) & DigA ((SDMin ((m + 2),m,k)),i) = 0 ) or ( DigA ((SDMin ((m + 2),m,k)),i) = DigA ((Mmin r),i) & DigA ((M0 r),i) = 0 ) )

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

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

A7: DigA ((M0 r),i) = M0Digit (r,i) by A3, Def2
.= 0 by A3, A6, Def1 ;
DigA ((Mmin r),i) = (- (Radix k)) + 1 by A1, A3, A4, A6, Def5
.= SDMinDigit (m,k,i) by A1, A5, A6, RADIX_5:def 1
.= DigA ((SDMin ((m + 2),m,k)),i) by A3, RADIX_5:def 2 ;
hence ( ( DigA ((M0 r),i) = DigA ((Mmin r),i) & DigA ((SDMin ((m + 2),m,k)),i) = 0 ) or ( DigA ((SDMin ((m + 2),m,k)),i) = DigA ((Mmin r),i) & DigA ((M0 r),i) = 0 ) ) by A7; :: thesis: verum

end;

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

A9: DigA ((SDMin ((m + 2),m,k)),i) = SDMinDigit (m,k,i) by A3, RADIX_5:def 2
.= 0 by A1, A8, RADIX_5:def 1 ;
DigA ((Mmin r),i) = r . i by A1, A3, A4, A8, Def5
.= M0Digit (r,i) by A3, A8, Def1
.= DigA ((M0 r),i) by A3, Def2 ;
hence ( ( DigA ((M0 r),i) = DigA ((Mmin r),i) & DigA ((SDMin ((m + 2),m,k)),i) = 0 ) or ( DigA ((SDMin ((m + 2),m,k)),i) = DigA ((Mmin r),i) & DigA ((M0 r),i) = 0 ) ) by A9; :: thesis: verum

end;

end;

end;

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

end;

m + 2 >= 1 by NAT_1:12;
hence (SDDec (Mmin r)) + (SDDec (DecSD (0,(m + 2),k))) = (SDDec (M0 r)) + (SDDec (SDMin ((m + 2),m,k))) by A1, A2, RADIX_5:15; :: thesis: verum