let i, n, k be Nat; :: thesis: for a being Tuple of n,k -SD st i in Seg n holds
DigA a,i is Element of k -SD
let a be Tuple of n,k -SD ; :: thesis: ( i in Seg n implies DigA a,i is Element of k -SD )
assume A1: i in Seg n ; :: thesis: DigA a,i is Element of k -SD
then a . i = DigA a,i by Def3;
hence DigA a,i is Element of k -SD by A1, Th18; :: thesis: verum