for m being Nat st m >= 1 holds
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