let i, n, k 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 )
assume A1: i in Seg n ; :: thesis: a . i is Element of k -SD
len a = n by FINSEQ_1:def 18;
then i in dom a by A1, FINSEQ_1:def 3;
then ( a . i in rng a & rng a c= k -SD ) by FINSEQ_1:def 4, FUNCT_1:def 5;
hence a . i is Element of k -SD ; :: thesis: verum