for i, n, k being Nat
for aSub being Tuple of n,k -SD_Sub st i in Seg n holds
DigA_SDSub (aSub,i) is Element of k -SD_Sub