let m be Nat; :: thesis: ( m >= 1 implies for n, k being Nat
for r being Tuple of m + 2,k -SD st k >= 2 & n in Seg (m + 2) & Mmask r is_Zero_over n & DigA (Mmask r),n > 0 holds
SDDec (Mmask r) > 0 )
assume m >= 1 ; :: thesis: for n, k being Nat
for r being Tuple of m + 2,k -SD st k >= 2 & n in Seg (m + 2) & Mmask r is_Zero_over n & DigA (Mmask r),n > 0 holds
SDDec (Mmask r) > 0
then A1: m + 2 >= 1 by Lm1;
let n, k be Nat; :: thesis: for r being Tuple of m + 2,k -SD st k >= 2 & n in Seg (m + 2) & Mmask r is_Zero_over n & DigA (Mmask r),n > 0 holds
SDDec (Mmask r) > 0
let r be Tuple of m + 2,k -SD ; :: thesis: ( k >= 2 & n in Seg (m + 2) & Mmask r is_Zero_over n & DigA (Mmask r),n > 0 implies SDDec (Mmask r) > 0 )
assume that
A2: k >= 2 and
A3: n in Seg (m + 2) and
A4: Mmask r is_Zero_over n and
A5: DigA (Mmask r),n > 0 ; :: thesis: SDDec (Mmask r) > 0
for i being Nat st i in Seg (m + 2) holds
DigA (Mmask r),i >= DigA (FSDMin (m + 2),n,k),i

proof

let i be Nat; :: thesis: ( i in Seg (m + 2) implies DigA (Mmask r),i >= DigA (FSDMin (m + 2),n,k),i )
assume A6: i in Seg (m + 2) ; :: thesis: DigA (Mmask r),i >= DigA (FSDMin (m + 2),n,k),i

now

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

suppose A7: i > n ; :: thesis: DigA (Mmask r),i >= DigA (FSDMin (m + 2),n,k),i

DigA (FSDMin (m + 2),n,k),i = FSDMinDigit n,k,i by A6, Def11
.= 0 by A2, A7, Def10 ;
hence DigA (Mmask r),i >= DigA (FSDMin (m + 2),n,k),i by A4, A7, Def12; :: thesis: verum

end;

suppose A8: i <= n ; :: thesis: DigA (Mmask r),i >= DigA (FSDMin (m + 2),n,k),i

now

per cases ( i = n or i < n ) by A8, XXREAL_0:1;

suppose A9: i = n ; :: thesis: DigA (Mmask r),i >= DigA (FSDMin (m + 2),n,k),i

then A10: DigA (Mmask r),i >= 0 + 1 by A5, INT_1:20;
DigA (FSDMin (m + 2),n,k),i = FSDMinDigit n,k,i by A6, Def11
.= 1 by A2, A9, Def10 ;
hence DigA (Mmask r),i >= DigA (FSDMin (m + 2),n,k),i by A10; :: thesis: verum

end;

suppose A11: i < n ; :: thesis: DigA (Mmask r),i >= DigA (FSDMin (m + 2),n,k),i

A12: DigA (Mmask r),i = (Mmask r) . i by A6, RADIX_1:def 3;
A13: (Mmask r) . i is Element of k -SD by A6, RADIX_1:18;
DigA (FSDMin (m + 2),n,k),i = FSDMinDigit n,k,i by A6, Def11
.= (- (Radix k)) + 1 by A2, A11, Def10 ;
hence DigA (Mmask r),i >= DigA (FSDMin (m + 2),n,k),i by A12, A13, RADIX_1:15; :: thesis: verum

end;

end;

end;

hence DigA (Mmask r),i >= DigA (FSDMin (m + 2),n,k),i ; :: thesis: verum

end;

end;

end;

hence DigA (Mmask r),i >= DigA (FSDMin (m + 2),n,k),i ; :: thesis: verum

end;

then SDDec (Mmask r) >= SDDec (FSDMin (m + 2),n,k) by A1, RADIX_5:13;
hence SDDec (Mmask r) > 0 by A2, A3, A1, Th19; :: thesis: verum