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

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