let i, n, k be Nat; :: thesis: 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
let aSub be Tuple of n,k -SD_Sub ; :: 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, Th11; :: thesis: verum