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

now

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, A3, A4, Def5
.= DigA r,i by A3, RADIX_1:def 3 ;
hence DigA r,i >= DigA (Mmin r),i ; :: thesis: verum

end;

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

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

end;

end;

end;

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

end;

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