let i, n, k be Nat; :: thesis: for aSub being Tuple of n, st i in Seg n holds
DigA_SDSub aSub,i is Element of k -SD_Sub
let aSub be Tuple of n, ; :: thesis: ( i in Seg n implies DigA_SDSub aSub,i is Element of k -SD_Sub )
assume A1: i in Seg n ; :: thesis: DigA_SDSub aSub,i is Element of k -SD_Sub
then aSub . i = DigA_SDSub aSub,i by Def5;
hence DigA_SDSub aSub,i is Element of k -SD_Sub by A1, Th12; :: thesis: verum