let m, k be Nat; :: thesis: ( k >= 2 implies for r being Tuple of m + 2,k -SD holds SDDec r >= SDDec (Mmin r) )
assume A1: k >= 2 ; :: thesis: for r being Tuple of m + 2,k -SD holds SDDec r >= SDDec (Mmin r)
let r be Tuple of m + 2,k -SD ; :: thesis: SDDec r >= SDDec (Mmin r)
for i being Nat st i in Seg (m + 2) holds
DigA (r,i) >= DigA ((Mmin r),i)

proof

let i be Nat; :: thesis: ( i in Seg (m + 2) implies DigA (r,i) >= DigA ((Mmin r),i) )
assume A2: i in Seg (m + 2) ; :: thesis: DigA (r,i) >= DigA ((Mmin r),i)
then A3: DigA ((Mmin r),i) = MminDigit (r,i) by Def6;

now :: thesis: DigA (r,i) >= DigA ((Mmin r),i)

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

suppose i >= m ; :: thesis: DigA (r,i) >= DigA ((Mmin r),i)

then DigA ((Mmin r),i) = r . i by A1, A2, A3, Def5
.= DigA (r,i) by A2, RADIX_1:def 3 ;
hence DigA (r,i) >= DigA ((Mmin r),i) ; :: thesis: verum

end;

suppose A4: i < m ; :: thesis: DigA (r,i) >= DigA ((Mmin r),i)

A5: DigA (r,i) = r . i by A2, RADIX_1:def 3;
A6: r . i is Element of k -SD by A2, RADIX_1:15;
DigA ((Mmin r),i) = (- (Radix k)) + 1 by A1, A2, A3, A4, Def5;
hence DigA (r,i) >= DigA ((Mmin r),i) by A5, A6, RADIX_1:13; :: thesis: verum

end;

end;

end;

hence DigA (r,i) >= DigA ((Mmin r),i) ; :: thesis: verum

end;

hence SDDec r >= SDDec (Mmin r) by NAT_1:12, RADIX_5:13; :: thesis: verum