:: deftheorem defines is_Zero_over RADIX_6:def 12 :
for n, m, k being Nat
for r being Tuple of m + 2,k -SD holds
( r is_Zero_over n iff for i being Nat st i > n holds
DigA (r,i) = 0 );