let i, k, n be Nat; :: thesis: for a being Tuple of n,k -SD st i in Seg n holds
a . i is Element of k -SD
let a be Tuple of n,k -SD ; :: thesis: ( i in Seg n implies a . i is Element of k -SD )
A1: len a = n by CARD_1:def 7;
assume i in Seg n ; :: thesis: a . i is Element of k -SD
then i in dom a by A1, FINSEQ_1:def 3;
then A2: a . i in rng a by FUNCT_1:def 3;
rng a c= k -SD by FINSEQ_1:def 4;
hence a . i is Element of k -SD by A2; :: thesis: verum