let i, n, k be Nat; for aSub being Tuple of n,k -SD_Sub st i in Seg n holds
DigA_SDSub (aSub,i) is Element of k -SD_Sub
let aSub be Tuple of n,k -SD_Sub ; ( i in Seg n implies DigA_SDSub (aSub,i) is Element of k -SD_Sub )
assume A1:
i in Seg n
; DigA_SDSub (aSub,i) is Element of k -SD_Sub
then
aSub . i = DigA_SDSub (aSub,i)
by Def5;
hence
DigA_SDSub (aSub,i) is Element of k -SD_Sub
by A1, Th11; verum