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