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

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