let i, k, n be Nat; for a being Tuple of n,k -SD st i in Seg n holds
DigA (a,i) is Element of k -SD
let a be Tuple of n,k -SD ; ( i in Seg n implies DigA (a,i) is Element of k -SD )
assume A1:
i in Seg n
; DigA (a,i) is Element of k -SD
then
a . i = DigA (a,i)
by Def3;
hence
DigA (a,i) is Element of k -SD
by A1, Th14; verum