let i, k, n 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, Th14; :: thesis: verum